RegroupingInvariance
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assert existence of a J or combiner satisfying the axioms.
- Does not derive the explicit RCL polynomial; that follows in a later theorem.
- Does not treat non-multiplicative or higher-dimensional comparison structures.
- Does not connect the axioms to specific physical constants or dimensions.
formal statement (Lean)
43structure RegroupingInvariance (J : ℝ → ℝ) extends ContextualSubstitutivity J where
44 symmetric : ∀ u v, combiner u v = combiner v u
45 zero_boundary : ∀ u, combiner u 0 = 2 * u
46 unit_diagonal : combiner 1 1 = 6
47 right_affine : ∀ u, ∃ α β, ∀ v, combiner u v = α * v + β
48
49/-- Contextual substitutivity is forced by the ledger's comparison
50structure: if `J(x₁) = J(x₂)`, then for any `y > 0`,
51
52 `J(x₁ y) + J(x₁/y) = J(x₂ y) + J(x₂/y)`
53
54because the compound cost depends only on the mismatch, not on the
55specific ratio realizing it. Therefore the compound cost descends
56to a function of `(J(x), J(y))`. -/