base_shift_denominator_scale_forced_no_hc_pos
plain-language theorem explainer
This theorem shows that equating base_shift to twice the canonical W term plus the cast rational (W + E_total) over (c E_passive) forces the scale c to equal exactly 4, without any positivity assumption on c. It would be cited in derivations that close the perturbative J-cost channel for mass ratios on the phi-ladder. The proof reduces the given equality to a prior ledger-fraction lemma by canonical decomposition, linear arithmetic, and exact rational casting.
Claim. If the base shift satisfies $base_shift = 2W + ((W + E_{total})/(c E_{passive}))$ (with the fraction cast to reals), then the denominator scale satisfies $c = 4$.
background
In the JCostPerturbation module the base_shift is the sum of a fixed 2W term and a ledger_fraction term that encodes the O4 perturbative correction. W is the canonical weight, E_total is the total cube-edge count (12), and E_passive is the passive-field edge count (11). These edge counts come from the SpectralEmergence.E definition E(D) = D * 2^(D-1) evaluated at D = 3. The upstream canonical arithmetic object supplies the initial Peano structure that makes the rational expressions well-defined and realization-independent.
proof idea
The tactic proof first uses simp to recover the canonical decomposition base_shift = 2W + ledger_fraction. It then applies linarith to the hypothesis and this decomposition to equate the fractional term to ledger_fraction in the reals. An exact_mod_cast lifts the equality back to rationals. The final step invokes the sibling lemma ledger_fraction_denominator_scale_forced_no_hc_pos to obtain c = 4.
why it matters
The result supplies the positivity-free closure for the denominator scale inside the mass-layer J-cost perturbation bridge. It supports the module's certification of the Jcost(1+alpha) channel form and the refined_shift decomposition, aligning with the Recognition Science phi-ladder mass formula and the eight-tick octave. Because used_by is currently empty it functions as an internal forcing lemma rather than a top-level export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.