ledger_forces_regrouping
plain-language theorem explainer
Given a cost function J on positive reals that vanishes at unity, is symmetric under inversion, has full range, and composes through an affine combiner P normalized at P(1,1)=6, this definition assembles the complete RegroupingInvariance structure. Researchers deriving the Recognition Composition Law from ledger axioms cite it to obtain the factorization gate. The body populates the structure fields directly from the supplied hypotheses together with the symmetry and boundary lemmas.
Claim. Let $J:ℝ→ℝ$ satisfy $J(1)=0$, $J(x)=J(x^{-1})$ for $x>0$, and surject onto $ℝ$. Let $P:ℝ→ℝ→ℝ$ satisfy $J(xy)+J(x/y)=P(J(x),J(y))$ for $x,y>0$, be right-affine in the second argument, and obey $P(1,1)=6$. Then the combiner $P$ is symmetric, satisfies the zero-boundary condition $P(u,0)=2u$, the unit-diagonal condition $P(1,1)=6$, and the right-affine property, so that $J$ obeys regrouping invariance.
background
The module establishes that contextual substitutivity together with regrouping invariance force the combiner to satisfy the FactorizationAssociativityGate, after which the RCL follows. RegroupingInvariance is the structure extending ContextualSubstitutivity J (if $J(x_1)=J(x_2)$ then $J(x_1 y)+J(x_1/y)=J(x_2 y)+J(x_2/y)$) by the four fields symmetric, zero_boundary, unit_diagonal, and right_affine. The upstream FactorizationAssociativityGate packages exactly those four properties on the combiner P. The hypotheses hSym, hJ0, hSurj, hComp, hAffine, and hP11 are the concrete ledger conditions that make the structure available.
proof idea
The definition is a direct constructor. It sets combiner to the supplied P and factors to the given composition law hComp. Symmetry of the combiner is obtained by applying the theorem combiner_symmetric. The zero-boundary condition is obtained by applying combiner_zero_boundary. The unit-diagonal value is taken directly from hP11. The right-affine property is taken directly from hAffine. The resulting record is returned as an instance of RegroupingInvariance J.
why it matters
This definition supplies the RegroupingInvariance package that produces a FactorizationAssociativityGate, which then forces the Recognition Composition Law exactly as stated in the module documentation. It therefore closes the step from primitive ledger properties (contextual substitutivity and regrouping invariance) to the RCL polynomial inside the Recognition Science derivation. The construction sits between the MagnitudeOfMismatch forcing structure and the downstream gate_forces_rcl step, touching the T5 J-uniqueness and RCL landmarks of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.