base_shift_weight_split_forced
plain-language theorem explainer
The theorem shows that rational weights a and b summing to 2 reproduce the canonical base_shift expression only when a equals 1 and b equals 1. Mass perturbation analysts working in the Recognition Science O4 closure would cite this to confirm uniqueness of the two-channel J-cost split. The proof reduces the given equality to the ledger_fraction_weight_split_forced lemma by linear arithmetic after rewriting the fractional term.
Claim. Let $a,b$ be rationals satisfying $a+b=2$. If base_shift equals $2W + (aW + b E_{total})/(4 E_{passive})$, then $a=1$ and $b=1$, where $W$, $E_{total}$, and $E_{passive}$ denote the weight and edge-count constants fixed by the mass anchor.
background
The Mass-Layer J-Cost Perturbation Bridge module supplies the O4 perturbative closure for mass-layer coefficients, including the Jcost(1+α) channel form and the α² + 12α³ radiative decomposition. Base_shift is defined as the sum of the canonical 2W term and the ledger_fraction term; E_passive abbreviates passive_field_edges D (11 for D=3) and E_total abbreviates cube_edges D (12). Upstream, the forces structure from MagnitudeOfMismatch guarantees single-valued comparison operators on any carrier, while band on StableState implements arithmetic conjunction via bit multiplication.
proof idea
The tactic proof first rewrites base_shift via simp to isolate the ledger_fraction term. Linarith then equates the supplied fractional expression to ledger_fraction over the reals. An exact_mod_cast lifts the equality to rationals, after which ledger_fraction_weight_split_forced is invoked directly on the sum hypothesis.
why it matters
This declaration certifies uniqueness inside the normalized two-weight family for base_shift, completing one step of the O4 coefficient forcing package in the Masses namespace. It aligns with the Recognition Science forcing chain by enforcing the self-similar fixed point under the eight-tick octave and D=3 edge counting. The module doc-comment positions the result as part of the explicit radiative decomposition used in refined_shift; no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.