regrouping_forces_gate
plain-language theorem explainer
Regrouping invariance for a cost function J implies that its combiner satisfies the four properties packaged in the factorization associativity gate. Derivations of the Recognition Composition Law from ledger axioms cite this bridge. The proof is a term-mode field projection that assembles the gate directly from the invariance structure.
Claim. Let $J : ℝ → ℝ$ and suppose $R$ is a regrouping invariance for $J$, so that its combiner $P$ is symmetric, right-affine, obeys $P(u,0)=2u$ for all $u$, and satisfies $P(1,1)=6$. Then $P$ satisfies the factorization associativity gate.
background
The LedgerFactorization module derives the Recognition Composition Law from contextual substitutivity and regrouping invariance. RegroupingInvariance J extends ContextualSubstitutivity J and requires the combiner to be symmetric, to obey the zero-boundary condition combiner u 0 = 2u, to normalize at the unit diagonal combiner 1 1 = 6, and to be right-affine. FactorizationAssociativityGate is the structure that packages exactly these four properties for any combiner P. The module setting states that these two ledger properties together force the combiner to satisfy the gate, after which gate_forces_rcl recovers the RCL polynomial.
proof idea
The proof is a term-mode construction. It supplies the four fields of FactorizationAssociativityGate by direct projection from the corresponding fields of RegroupingInvariance: symmetric from R.symmetric, rightAffine from R.right_affine, zeroBoundary from R.zero_boundary, and unitDiagonal from R.unit_diagonal.
why it matters
This is the second half of Bridge B2. It feeds the downstream ledger_forces_rcl, which applies gate_forces_rcl to obtain the explicit RCL combiner P(u,v) = 2uv + 2u + 2v. The declaration closes the unconditional path from ledger substitutivity and regrouping to the Recognition Composition Law inside the DAlembert factorization layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.