base_shift_kn_forced_under_passive_bound
plain-language theorem explainer
The theorem shows that equating the base shift to 2W plus the rational perturbation term ((W + E_total + n)/(k E_passive)) under the constraints k > 0 and n ≤ E_passive forces the unique solution k = 4 and n = 0. Mass-layer modelers in Recognition Science cite this when closing perturbative expansions to integer rung assignments on the phi-ladder. The proof reduces the given equality to the ledger-fraction form by canonical simplification and linear arithmetic, then invokes the sibling forcing lemma.
Claim. Let $k,n$ be natural numbers with $k>0$ and $n≤E_{passive}$. If the base shift equals $2W + ((W + E_{total} + n)/(k E_{passive}))$, then $k=4$ and $n=0$.
background
The module supplies the O4 perturbative closure for J-cost perturbations in the mass layer. Base shift is defined as the canonical 2W plus ledger-fraction term; ledger_fraction is the rational (W + E_total + n)/(k E_passive) that encodes integer numerator/denominator shifts. E_passive abbreviates the passive edge count (11) and E_total the total cube edges (12) from the D-cube geometry in SpectralEmergence.E and Anchor. W is the active-edge weight from the Anchor module. The local setting is the J-cost bridge that ties these integer perturbations to the Recognition Composition Law and the phi-ladder mass formula.
proof idea
Tactic proof. First simp reduces the hypothesis to the canonical base_shift = 2W + ledger_fraction form. Linear arithmetic then equates the rational perturbation term to ledger_fraction over the reals. Exact cast lifts the equality to rationals. The final exact step applies the sibling lemma ledger_fraction_kn_forced_under_passive_bound.
why it matters
It packages the integer-forcing step that closes the O4 coefficient channel in the mass-layer J-cost bridge, ensuring perturbative shifts remain on the discrete phi-ladder without explicit positivity hypotheses. The result sits inside the T5–T6 forcing chain that derives J-uniqueness and the self-similar fixed point, feeding the eight-tick octave and D=3 geometry. No downstream uses are recorded yet; it directly supports refined_shift and the alpha-band derivations in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.