balance_constraint_codim_1
plain-language theorem explainer
The theorem establishes that the dual-balance codimension of the ledger constraint surface equals one. Researchers deriving the curvature correction term in the fine-structure constant would cite this to confirm the five-dimensional phase space that produces the π^5 factor. The proof is a direct reflexivity reduction on the explicit definition of the codimension.
Claim. The codimension of the dual-balance constraint surface equals $1$.
background
The Curvature Space Derivation module accounts for the ledger state in a five-dimensional configuration space: three spatial dimensions on the cubic lattice, one temporal dimension from the eight-tick cycle, and one dual-balance dimension from the conserved quantity σ. The dual-balance codimension is defined as the codimension of the constraint surface and set to one. This choice ensures each dimension contributes a π factor from angular integration, producing the observed denominator 102π^5 in the curvature correction δ_κ = -103/(102π^5).
proof idea
The proof is a one-line wrapper that applies reflexivity directly to the definition dual_balance_codimension := 1.
why it matters
This result completes the dimension count for the phase-space integration underlying the curvature correction in α^{-1} = 4π·11 - f_gap - 103/(102π^5). It supplies the dual-balance component alongside the three spatial dimensions forced by T8 and the temporal dimension from the eight-tick octave. The theorem thereby fixes the precise power of π that appears in the fine-structure constant formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.