ledger_fraction_eq_29_over_44
plain-language theorem explainer
The canonical ledger fraction in the electron-break base shift equals exactly 29/44. Researchers closing O4 coefficient slots in the J-cost perturbation bridge for lepton masses cite this rational value when assembling the refined shift. The proof is a one-line computational decision that evaluates the ledger_fraction definition directly.
Claim. In the J-cost perturbation framework the ledger fraction for the electron-break base shift satisfies $29/44$.
background
J-cost is the cost function on positive reals supplied by the PhiForcingDerived structure and obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Ledger factorization is the structure of (R_+, ×) with J-calibration given by DAlembert.LedgerFactorization. The module supplies the mass-layer bridge that certifies the Jcost(1+α) perturbative channel and the explicit α² + 12α³ radiative decomposition. Upstream, SpectralEmergence forces the gauge content SU(3)×SU(2)×U(1) together with exactly three generations, while NucleosynthesisTiers places nuclear densities on discrete φ-tiers.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality ledger_fraction = 29/44.
why it matters
This supplies the exact rational used in base_shift_eq_34_plus_29_over_44 to write the zeroth-order geometric part of the refined shift as 34 + 29/44. It is invoked inside o4_slot_forcing_certificate to close the primary coefficient slots for the lepton chain. The value pins the ledger fraction at the canonical phi-ladder step for the electron-break, consistent with T5 J-uniqueness and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.