ledger_fraction_kn_forced_under_passive_bound
plain-language theorem explainer
Any integer perturbation matching the canonical ledger fraction under the passive band forces the multiplier k to exactly 4 and the offset n to exactly 0. Mass-layer modelers closing O4 perturbative channels cite this Diophantine constraint when pinning J-cost coefficients. The argument substitutes the fixed topology counts, clears denominators via field simplification, and solves the resulting linear equation with integer arithmetic.
Claim. Suppose $k,n$ are natural numbers with $k>0$ and $n$ at most the passive edge count. If $(W+E_0+n)/(k E_p)$ equals the canonical ledger fraction, then necessarily $k=4$ and $n=0$.
background
The module bridges J-cost perturbations to canonical lepton steps and certifies the O4 coefficient channel form together with its radiative decomposition. Mass topology fixes the constants W=17, E_total=12, E_passive=11 that appear in the fraction. Upstream arithmetic lemmas from ArithmeticFromLogic supply associativity and commutativity for the Nat-to-ℚ rewrites, while the edge-count definition E from SpectralEmergence supplies the passive band size.
proof idea
Extract the three topology constants from mass_topology_counts. Rewrite the hypothesis to ((29+n)/(k·11))=29/44, clear the denominator with field_simp, and obtain the cross-multiplied relation 44(29+n)=29(k·11) by nlinarith. The bound n≤11 together with linear integer arithmetic then forces the unique solution k=4, n=0.
why it matters
The result supplies the core forcing step for ledger-fraction perturbations and directly feeds both the base_shift closure and its positivity-free sibling. It completes the integer-band constraint inside the O4 perturbative package, aligning the mass-layer bridge with the Recognition Science phi-ladder mass formula. The proof is fully closed with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.