base_shift_numerator_offset_forced
plain-language theorem explainer
The theorem shows that fixing the canonical 2W term in base_shift forces the numerator offset n to vanish when the expression matches the normalized ledger fraction form 2W + ((W + E_total + n)/(4 E_passive)). Researchers closing the O4 perturbative coefficients in the Recognition Science mass layer would cite it to confirm the (1,1) split in the two-weight family. The proof reduces the hypothesis by simplification and linear arithmetic to a prior ledger fraction lemma.
Claim. If $base_shift = 2W + ((W + E_{total} + n)/(4 E_{passive}))$ holds with the canonical 2W term fixed, then $n = 0$, where $W$, $E_{total}$, and $E_{passive}$ denote the wallpaper group count, total cube edges, and passive edge count.
background
The Mass-Layer J-Cost Perturbation module upstreams the O4 perturbative closure into the Masses namespace and certifies the Jcost(1+α) channel form together with the explicit α² + 12α³ radiative decomposition. Base shift is expressed as 2W plus a ledger fraction term, with constants taken from the Anchor module: W = wallpaper_groups (17), E_total = cube_edges D (12), E_passive = passive_field_edges D (11). Upstream, the canonical arithmetic object supplies the realization-independent Peano structure, while the magnitude-of-mismatch structure enforces single-valued comparison on any carrier.
proof idea
The tactic proof first applies simp to rewrite base_shift as 2W plus ledger_fraction. It then uses linarith on the hypothesis and the rewritten form to equate the fractional term to ledger_fraction in reals, casts the equality back to rationals, and invokes the sibling lemma ledger_fraction_numerator_offset_forced to obtain n = 0.
why it matters
The result locks the numerator offset in the two-weight family, feeding the sibling ledger_fraction equations and mass_topology_counts that close the O4 coefficient forcing. It sits inside the Recognition Science mass-ladder construction, where the phi-ladder mass formula and eight-tick octave already fix the geometric constants; this step eliminates free parameters in the perturbative bridge. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.