This document provides a variational physics formulation of the Quantum Logical Framework (QLF) using the principle of zero action.
In QLF's possibilist ontology, ℒ = 0 is not a filter applied to a pre-existing universe — it is the condition of origin itself. The universe IS what achieves Zero Free Action. Histories without ZFA closure are not eliminated from existence; they never had it. See Philosophy.md for the full possibilist foundation and TheBigProblem.md for how this resolves the measurement problem, spacetime, and gravity without additional postulates.
The foundation of QLF is expressed through a vanishing Lagrangian density:
S = ∫ ℒ dΩ, with ℒ = 0
This null action principle replaces traditional stationary action (δS = 0) with an identically zero Lagrangian. Only configurations satisfying ℒ = 0 are logically persistent.
Discrete primary form. In QLF, the fundamental formulation is discrete. The 8-twist alphabet {^, v, <, >, /, \, +, −} (see QuCalc.md and eight-twists-sufficiency.md) generates event histories whose imbalance is tracked component-wise by computeImbalance (ZFAEventDynamics.lean:90). ZFA closure requires all 8 counts to vanish simultaneously:
isZFAClosed h ↔ ∀ i : Fin 8, computeImbalance h i = 0
Continuous limit. The continuous Lagrangian emerges through EventSynthesisField, which carries a scalar field φ, its time derivative, and potential V_φ. These map to the stress-energy tensor and effective cosmological constant Λ_eff (SpacetimeDynamics.lean:57), recovering Einstein-like field equations in the continuum limit. See SpaceTime.md for the event-synthesis picture and Gravity.md for emergent gravity from ZFA event rate and gauge-fold depth.
Machine-verified anchor. rho_process_always_zfa (RhoQuCalc.lean:382) proves that every constructible RhoProcess satisfies the variational condition unconditionally — it is impossible to build a ZFA-violating process within the algebra.
The condition ∂ₜ|ψ⟩ = 0 enforces continuous quantum Zeno dynamics. In the short-time limit, the time evolution operator satisfies:
lim_{t→0} U(t) = 𝕀
This freezes the quantum state, preventing evolution away from the zero-action manifold.
In QLF, the stable states satisfying this condition are computed exactly by find_stable_states (QLF_QuCalc.lean:35). Two machine-verified theorems characterize them:
find_stable_states_iff(QLF_Riemann.lean:118): a string is stable if and only if it is a symmetric pure-phase string — the precise ZFA formulation of ∂ₜ|ψ⟩ = 0.find_stable_states_length_even(QLF_Riemann.lean:293): there are exactly C(2n, n) stable states at depth 2n — the same combinatorial count appearing in string mode degeneracy and the Riemann zeta critical line.
The symmetry structure is carried by the eight-generator algebra:
Σ₈ = {τ¹ … τ⁸}
with the full product rule (machine-verified via tau_xy_product, tau_yz_product, tau_zx_product in lean/BraKetRhoQuCalc.lean):
τᵢ τⱼ = −δᵢⱼ I − εᵢⱼₖ τₖ
This gives commutator [τᵢ, τⱼ] = −2 εᵢⱼₖ τₖ and anti-commutator {τᵢ, τⱼ} = −2 δᵢⱼ I.
Note: with τᵢ = iσᵢ, products are anti-cyclic (τxτy = −τz, not +τz). The cyclic convention τxτy = +τz would require τᵢ = −iσᵢ. Both conventions encode the same commutator algebra up to overall sign; QLF uses τᵢ = iσᵢ throughout (machine-verified: tau_x_sq, tau_xy_product etc.).
Relation to QLF's Pauli algebra. QLF's Form structure (SpacetimeDynamics.lean) uses the Pauli basis with σᵢ² = I (not −I) and [σᵢ, σⱼ] = 2i εᵢⱼₖ σₖ (machine-verified: sigma_comm_xy, sigma_comm_yz, sigma_comm_zx in lean/BraKetRhoQuCalc.lean). The connection is τᵢ = i σᵢ: the Σ₈ generators are the Pauli matrices multiplied by i. Both algebras encode 8 degrees of freedom; only the sign of the square differs (quaternionic τᵢ² = −I vs Hermitian σᵢ² = I). QLF's 8-twist alphabet organizes these as 4 Hermitian-conjugate pairs. The density-matrix realization of this algebra — how Form maps to bra-ket notation — is worked out in BraKetRhoQuCalc.md and machine-verified in lean/BraKetRhoQuCalc.lean. The Pauli exclusion consequence (fermionic antisymmetry via matrix commutator) is proved in lean/PauliExclusion.lean.
This algebra provides the non-commutative structure that protects valid logical distinctions.
Real-time pruning removes any component that violates the zero-action condition. This is implemented by full_zeno_prune (QLF_Axioms.lean), which eliminates all TopoStrings with unbalanced phase counts.
Two machine-verified theorems establish that this is a selection, not a restriction:
encode_is_zfa(QLF_Universality.lean:60): every terminating computation encodes as a ZFA-closed string — nothing computable is pruned.qlf_universality(QLF_Universality.lean:74): the ZFA filter is Church-Turing complete. Whatfull_zeno_pruneeliminates is precisely the physically unrealizable tail — non-terminating, Busy Beaver-class computations that never achieve closure. See Universality.md for the full argument and ReverseMathematics.md for why the core operates in RCA₀ below the Busy Beaver horizon.
Only states that remain consistent with ℒ = 0 persist. This implements QLF's core rule: asymmetric distinctions are pruned.
The security conditions are:
[H, ρ_S] = 0
Tr(ρ_S ρ_E) = 0
These ensure the system state is a constant of motion and orthogonal to the environment.
Machine-verified anchors:
rho_process_always_symmetric(RhoQuCalc.lean:388): every RhoProcess lies on the critical line (is_symmetric) — the ZFA formulation of[H, ρ_S] = 0.commutator_zero_diagonal(BraKetRhoQuCalc.lean): for any Form f with f.x = f.y = 0 (diagonal in the σz basis),[σz, f.toMatrix] = 0— the matrix-level proof of[H, ρ_S] = 0for ZFA-symmetric states. Corollaries:commutator_zero_ket0_sigmaz,commutator_zero_ket1_sigmaz.orthogonality_01(BraKetRhoQuCalc.lean:173): ρ₁ · ρ₀ = 0, machine-verified by matrix computation — the density-matrix formulation of Tr(ρ_S ρ_E) = 0 for orthogonal basis states.bra_ket_always_balanced(BraKetRhoQuCalc.lean:109): it is impossible to construct a ZFA-unbalanced RhoProcess — the type system enforces the security condition at construction time.decoherence_impossibility(BraKetRhoQuCalc.lean): parallel composition (ρ_S ⊗ env) is always ZFA-closed — no decoherence event is algebraically constructible.spectral_gap_zero_iff_symmetric(QLF_Spectral.lean): the spectral gap|count_pos − count_neg|vanishes iff the string is ZFA-symmetric — eigenvalue-level proof that all ZFA-symmetric states have degenerate spectra (scalar × I). See SpectralGap.md for the connection to Wigner-Dyson spacing and Maxwell's Gauss duality.
Any decohering interaction would require violating either the zero-action condition or the algebraic structure. Since both are enforced by construction and machine-verified, decoherence is a logical contradiction rather than environmental noise. See Measurement_Problem.md for the full treatment of measurement as ZFA closure, and ER_EPR_QLF.md for the entanglement-geometry connection.
The stationary variation of the Lagrangian defines the quantum processing unit core:
δℒ = 0
The fundamental object of the system is given by:
Φ₀ = U + M, where U = ℒ and M = Σ₈
In RhoProcess terms: U is the ZFA closure condition (the action component, satisfied by rho_process_always_zfa), and M is the twist algebra (the symmetry component, carried by the action/lift/parallel/sequence/dagger constructors). Every physical process is a Φ₀-structured object. See QuantumOS.md for how this maps to a capability-secure OS kernel for QPUs.
| Concept | Lean source | Prose |
|---|---|---|
| ZFA imbalance closure | lean/ZFAEventDynamics.lean | SpaceTime.md, Gravity.md |
| Form / Pauli algebra | lean/SpacetimeDynamics.lean | BraKetRhoQuCalc.md |
| ρ-process algebra / ZFA | lean/RhoQuCalc.lean | lean/README.md |
| Bra-ket ↔ RhoQuCalc | lean/BraKetRhoQuCalc.lean | BraKetRhoQuCalc.md |
| Pauli exclusion / Σ₈ antisymmetry | lean/PauliExclusion.lean | — |
| 8-twist alphabet | lean/QLF_Axioms.lean | QuCalc.md, eight-twists-sufficiency.md |
| Stable-state count C(2n,n) | lean/QLF_QuCalc.lean, lean/QLF_Riemann.lean | Riemann-Conjecture-Proof.md |
| String mode degeneracy | lean/StringTheoryQLF.lean | StringTheory.md |
| Church-Turing universality | lean/QLF_Universality.lean | Universality.md, ReverseMathematics.md |
| Measurement / decoherence | lean/BraKetRhoQuCalc.lean (decoherence_impossibility, commutator_zero_diagonal) |
Measurement_Problem.md, TheBigProblem.md |
| Entanglement / ER=EPR | lean/ER_EPR_QLF.lean | ER_EPR_QLF.md |
| Possibilist origin / ZFA | — | Philosophy.md, TheContinuum.md |
| QPU / security / OS | — | QuantumOS.md |
This formulation shows that QLF's Zero Free Action principle can be expressed variationally as a null Lagrangian. Decoherence becomes mathematically impossible within this framework, as it would require violating either the zero-action condition or the algebraic structure — both enforced by construction and machine-verified.
The Lagrangian formulation provides a bridge between the distinction-based language of QLF and standard physics notation, with every claim anchored in a specific machine-verified Lean theorem.
See also: Langlands.md — the Σ₈ algebra developed here is the elementary-representation source for the QLF-as-bottom-up-Langlands scaffolding; tau_xy_product etc. are read there as the Langlands product relations; Active_Inference_Mathematics.md — the Σ₈ algebra surfaces in the meta as the Pauli closure half of ZFA, completing the single rule of active-inference math (§2 of the meta-doc).