ledger_forces_rcl
plain-language theorem explainer
Ledger substitutivity together with regrouping invariance forces the combiner to equal the RCL polynomial 2uv + 2u + 2v. Workers deriving the Recognition Composition Law cite this as the unconditional bridge from the two ledger primitives. The proof is a one-line term that applies gate_forces_rcl after regrouping_forces_gate has supplied the FactorizationAssociativityGate.
Claim. If a combiner $P : ℝ → ℝ → ℝ$ satisfies the regrouping invariance conditions (symmetry, zero boundary $P(u,0)=2u$, unit diagonal $P(1,1)=6$, and right-affine form) that follow from contextual substitutivity of a cost function $J$, then $P(u,v)=2uv+2u+2v$ for all real $u,v$.
background
RegroupingInvariance is a structure extending ContextualSubstitutivity J. It requires the combiner to be symmetric, obey zero_boundary (∀u, combiner u 0 = 2u), unit_diagonal (combiner 1 1 = 6), and right_affine (for each u there exist α, β such that combiner u v = α v + β for all v). The module proves that contextual substitutivity and regrouping invariance together force the combiner to obey the FactorizationAssociativityGate. Upstream, gate_forces_rcl states that canonical normalization selects the RCL member of the bilinear family, while regrouping_forces_gate shows that the invariance package produces exactly that gate.
proof idea
The proof is a one-line term wrapper. It supplies R.combiner together with the FactorizationAssociativityGate produced by regrouping_forces_gate J R directly to gate_forces_rcl.
why it matters
This declaration completes Bridge B2, delivering the Recognition Composition Law polynomial directly from the two ledger primitives. It sits downstream of regrouping_forces_gate and gate_forces_rcl, and supplies the explicit form required for J-uniqueness (T5) and the phi-ladder mass formula in the forcing chain. No open questions or scaffolding remain at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.