ledger_fraction_denominator_forced
plain-language theorem explainer
The normalized geometric ratio (W + E_total) over (k times E_passive) matching the canonical ledger fraction forces the positive integer k to equal 4. Mass-layer calculations in Recognition Science cite this to fix the denominator scaling inside the J-cost expansion. The tactic proof extracts the fixed counts W=17, E_total=12, E_passive=11 from the topology lemma, reduces the hypothesis to the ratio comparison 29 over 11k equaling 29 over 44, and applies the dedicated forcing lemma.
Claim. Let $k$ be a positive integer. If the normalized ratio $(W + E_0)/(k E_p)$ equals the canonical ledger fraction, then $k=4$.
background
The J-cost perturbation module bridges mass-layer coefficients to canonical lepton-step definitions and certifies the perturbative channel form together with exact zeroth-order geometric evaluations. W is the wallpaper-group count 17, E_total the total cube edges 12, and E_passive the passive field edges 11; these arise from the D-cube edge formula E(D) = D * 2^(D-1) with D=3 and the passive subtraction of one active edge per tick. The upstream canonical arithmetic object supplies the realization-independent Peano structure, while the magnitude-of-mismatch structure enforces single-valued comparisons on any carrier.
proof idea
The proof extracts W=17, E_total=12 and E_passive=11 directly from the mass_topology_counts lemma. It substitutes these values into the hypothesis and normalizes to obtain the equality 29/(11k) = 29/44. It then applies the ratio_29_over_11k_forces_k_eq_four lemma to conclude k=4.
why it matters
This theorem supplies the denominator-forcing step required by the O4 perturbative closure in the mass layer. It feeds base_shift_denominator_forced, which augments the ratio by the 2W term, and the positivity-free variant. Within the Recognition framework it pins the integer k=4 demanded by the eight-tick octave and the phi-ladder mass formula, ensuring the J-cost expansion matches the canonical ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.