RegroupingInvariance
plain-language theorem explainer
RegroupingInvariance packages the symmetry, zero-boundary, unit-diagonal, and right-affine properties of the combiner that follow from the abelian group structure on positive reals together with J-calibration. Researchers deriving the Recognition Composition Law from ledger axioms cite it when closing the bridge from contextual substitutivity to the factorization gate. The declaration is a structure extension of ContextualSubstitutivity that adjoins exactly those four axioms on the combiner.
Claim. Let $J : ℝ → ℝ$. A regrouping invariance structure on $J$ consists of a combiner $P : ℝ → ℝ → ℝ$ such that $J(xy) + J(x/y) = P(J(x), J(y))$ for all $x, y > 0$, together with the axioms $P(u,v) = P(v,u)$, $P(u,0) = 2u$, $P(1,1) = 6$, and the right-affine condition that for each $u$ there exist scalars $α, β$ with $P(u,v) = α v + β$ for all $v$.
background
Contextual substitutivity states that the compound cost of a pair depends only on the individual J-costs, so the combiner descends to a function of $(J(x), J(y))$. Regrouping invariance adds the symmetry, boundary, and affinity conditions forced by the multiplicative group structure on positive reals and the normalization $J(1) = 0$. The module uses these two primitives to obtain the Recognition Composition Law via an associativity gate. Upstream results supply the cost functions from multiplicative recognizers and observer forcing, where J-cost quantifies mismatch in recognition events.
proof idea
This is a structure definition with an empty proof body. It extends ContextualSubstitutivity by adjoining the four field axioms symmetric, zero_boundary, unit_diagonal, and right_affine directly on the combiner.
why it matters
RegroupingInvariance supplies the second primitive for ledger factorization. It is invoked by regrouping_forces_gate to produce the FactorizationAssociativityGate and by ledger_forces_rcl to obtain the explicit RCL form $P(u,v) = 2uv + 2u + 2v$. In the Recognition Science framework this step converts the two ledger invariances into the functional equation that defines the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.