ledger_fraction_weight_split_forced
plain-language theorem explainer
The theorem shows that rational weights a and b summing to 2 must each equal 1 when their weighted combination of W and E_total divided by 4 E_passive matches the ledger fraction. Mass-layer modelers in Recognition Science cite it to fix the canonical split inside J-cost perturbations. The proof substitutes the concrete topology values W=17, E_total=12, E_passive=11 and solves the resulting linear system by cross-multiplication followed by nlinarith.
Claim. Let $a,b$ be rational numbers with $a+b=2$. If $(aW + b E_0)/(4E_p)$ equals the ledger fraction, where $W$, $E_0$ and $E_p$ are the fixed mass-topology counts, then necessarily $a=1$ and $b=1$.
background
Recognition Science places masses on the phi-ladder via J-cost perturbations. The ledger fraction is the normalized two-channel weight $(aW + bE)/(4E_p)$ inside the passive-edge band. The JCostPerturbation module supplies the O4 perturbative closure by linking these weights to canonical lepton-step definitions and the arithmetic object supplied by upstream ArithmeticOf.canonical. It draws on NucleosynthesisTiers.of for the discrete phi-tier densities and on PhiForcingDerived.of together with PreLogicalCost.band for the underlying J-cost and stable-state arithmetic.
proof idea
The tactic proof first pulls W=17, E_total=12 and E_passive=11 from mass_topology_counts. Substitution into the hypothesis produces the simplified linear relation (17a + 12b)/44 = 29/44. Cross-multiplication followed by nlinarith yields 17a + 12b = 29. A second nlinarith step with the sum constraint a + b = 2 then isolates a=1 and b=1.
why it matters
The result is invoked directly by base_shift_weight_split_forced to enforce the canonical (1,1) split inside the base-shift expression. It completes one step of the O4 coefficient forcing inside the J-cost perturbative channel, consistent with the phi-ladder mass formula and the eight-tick octave. The module doc-comment notes that the same path supplies exact geometric evaluations of the zeroth-order constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.