base_shift_kn_forced_under_passive_bound_no_hk
plain-language theorem explainer
Under the passive edge bound n ≤ E_passive, equality of the base shift to 2W plus the explicit fractional term ((W + E_total + n)/(k E_passive)) forces k=4 and n=0. Mass topology derivations in the Recognition framework cite this to pin the integer parameters in O4 coefficient forcing without separate positivity checks. The tactic proof rewrites the base shift definition, equates the fractional term via linarith, casts to rationals, and reduces directly to the ledger fraction forcing lemma.
Claim. If $n ≤ E_{passive}$ and the base shift equals $2W + ((W + E_{total} + n)/(k E_{passive}))$, then $k=4$ and $n=0$.
background
The Mass-Layer J-Cost Perturbation module upstreams the O4 perturbative closure and defines base_shift as 2W + ledger_fraction, where W is the wallpaper group count (17) and E_total the total cube edges (12). E_passive is the passive edge count (11). The ledger_fraction term is the rational ((W + E_total + n)/(k E_passive)) cast to reals, matching the form used in mass topology.
proof idea
The proof rewrites base_shift via its definition to isolate ledger_fraction. Linarith equates the given fractional expression to ledger_fraction in reals. Exact casting to rationals produces the hypothesis for the sibling lemma ledger_fraction_kn_forced_under_passive_bound_no_hk, which is applied directly together with the bound hn_le.
why it matters
This packages the positivity-free base_shift closure for integer perturbations, supporting the mass topology path and O4 coefficient forcing in the Recognition framework. It fixes k=4 and n=0 under the passive band without explicit positivity on k, consistent with the J-cost perturbative channel and the α² + 12α³ radiative decomposition certified in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.