ledger_fraction_denominator_scale_forced
plain-language theorem explainer
The theorem shows that matching the canonical ledger fraction forces the positive rational scale c in (W + E_total)/(c E_passive) to equal exactly 4. Mass-layer researchers cite it to close the denominator scale in O4 perturbative coefficient forcing. The proof substitutes the fixed topology counts W=17, E_total=12, E_passive=11, reduces the equality to 29/(11c)=29/44, and concludes via cross-multiplication followed by linear arithmetic.
Claim. Let $W$, $E_0$, $E_p$ denote the wallpaper, total-edge, and passive-edge counts. If $c$ is a positive rational satisfying $(W + E_0)/(c E_p)$ equals the canonical ledger fraction, then $c=4$.
background
The module supplies the Lean closure for O4 coefficient forcing in the mass layer. It certifies the J-cost(1+α) perturbative channel form together with the explicit α² + 12α³ radiative decomposition and the zeroth-order geometric constants. E_passive is the passive-field edge count (passive_field_edges D, equal to 11 for D=3). W is the wallpaper-group count (17). E_total is the total edge count (12). These three integers are supplied by the sibling mass_topology_counts. The ledger fraction is the canonical ratio 29/44 obtained from the two-channel J-cost decomposition in the same module.
proof idea
The tactic proof first extracts W=17, E_total=12, E_passive=11 from mass_topology_counts. It rewrites the hypothesis via simpa and mul_comm to obtain the raw equality (29)/(11c) = 29/44. Norm_num simplifies the right-hand side. Cross-multiplication via div_eq_div_iff produces the integer equation 29·44 = 29·(11c). nlinarith then yields c=4.
why it matters
The result pins the rational denominator scale inside the mass-layer J-cost perturbation bridge, completing one of the explicit coefficient-forcing steps certified by the module. It sits downstream of the canonical arithmetic and spectral-edge counts (E, passive_field_edges) and upstream of any further ledger-fraction identities in the O4 closure. The declaration therefore supplies a concrete numerical anchor for the phi-ladder mass formula at the lepton step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.