base_shift_denominator_forced_no_hk
plain-language theorem explainer
Equating the base shift to twice the weight W plus the term (W + E_total) over (k times E_passive) forces the integer parameter k to equal 4. This holds without any positivity assumption on k. Researchers closing the O4 perturbative J-cost channel for lepton masses cite the result when fixing the denominator in the mass ladder. The proof reduces the given equality to an equivalent ledger fraction statement via linear arithmetic and then invokes the sibling denominator forcing lemma.
Claim. If the base shift equals $2W + (W + E_{total})/(k E_{passive})$, then $k=4$.
background
The module bridges mass-layer J-cost perturbations to canonical lepton-step definitions and certifies the Jcost(1+α) perturbative channel form together with the α² + 12α³ radiative decomposition. Base shift is expressed as the canonical 2W term plus a ledger fraction; the ledger fraction itself is the rational (W + E_total)/(k E_passive) with E_total and E_passive drawn from the anchor definitions. Upstream results supply the edge count E(D) = D * 2^(D-1) for the D-cube and the realization-independent canonical arithmetic object whose Peano surface supplies the invariant arithmetic content used in the fraction manipulations.
proof idea
The tactic proof first applies simp to rewrite the hypothesis as base_shift = 2W + ledger_fraction. Linear arithmetic then equates the rational term in the hypothesis to the ledger fraction in reals. An exact_mod_cast step lifts the equality to rationals, after which the sibling lemma ledger_fraction_denominator_forced_no_hk is applied directly.
why it matters
The declaration supplies the positivity-free closure for the base-shift denominator inside the J-cost perturbation bridge, supporting the O4 coefficient forcing package. It aligns with the phi-ladder mass formula by fixing the rung parameter k=4 and with the eight-tick octave structure through the ledger fraction that appears in the mass topology counts. No downstream theorems yet invoke it, leaving the result available for future ledger-fraction derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.