Foundation Dalembert Ledger Factorization Regrouping Invariance

Regrouping invariance

Regrouping invariance is a property a comparison system might have: when you compare three items, the total cost should not depend on which pair you compare first. In ordinary arithmetic, this is like saying (a + b) + c equals a + (b + c). The Recognition Science framework studies this property in a setting where each comparison carries a cost, and it asks what forms of cost function are compatible with such regrouping freedom.

The framework's machine-checked library of formal theorems proves that regrouping invariance, together with a second property called contextual substitutivity, forces the comparison cost to obey a specific algebraic law. Contextual substitutivity says that if two subcomparisons have the same cost, they can be swapped inside any larger comparison without changing the total. Regrouping invariance adds that the order of combining three comparisons does not matter. From these two, the library derives that the cost combiner must satisfy the equation P(u, v) = 2uv + 2u + 2v for any two costs u and v.

This equation is not chosen; it is forced. The proof proceeds by showing that the two primitive properties imply a set of conditions on the combiner, such as symmetry and a boundary condition, and those conditions in turn pin down the combiner uniquely. The result is a theorem in the library, meaning it is checked by a machine against a fixed set of axioms. It does not rely on any additional assumptions about what the cost function should be.

What the declaration does not claim is important. It does not claim that every possible comparison system satisfies regrouping invariance; it only says that if a system does satisfy it, along with contextual substitutivity, then the combiner must have that form. It also does not claim that the cost function itself is unique. The theorem concerns the combiner, the rule for putting two costs together, not the underlying cost function J. Finally, it does not claim that the right-affine condition, which is part of the regrouping package, is proved from the primitive properties alone; in the library it is encoded as a hypothesis on the combiner, with the derivation left as a paper argument.

The practical consequence is that the framework has a precise, machine-checked handle on how comparison costs must combine if they are to be well behaved under regrouping. This is one step in a longer chain that leads to the framework's account of physical structure, but the step itself is narrow and fully specified.

/-- **Bridge B2 (unconditional)**: from ledger substitutivity and
regrouping, the RCL combiner `P(u,v) = 2uv + 2u + 2v` is forced. -/
theorem ledger_forces_rcl
    (J : ℝ → ℝ) (R : RegroupingInvariance J) :
    ∀ u v, R.combiner u v = 2 * u * v + 2 * u + 2 * v :=
  gate_forces_rcl R.combiner (regrouping_forces_gate J R)

/-- **Bridge B2 (unconditional)**: from ledger substitutivity and
regrouping, the RCL combiner `P(u,v) = 2uv + 2u + 2v` is forced. -/
theorem ledger_forces_rcl
    (J : ℝ → ℝ) (R : RegroupingInvariance J) :
    ∀ u v, R.combiner u v = 2 * u * v + 2 * u + 2 * v :=
  gate_forces_rcl R.combiner (regrouping_forces_gate J R)

/-- From a zero-parameter comparison ledger with admissible cost
and surjective cost range, the full regrouping-invariance package
is available.  The right-affine response follows from the
triple-identity / strict-convexity argument (proved in the paper;
encoded here as a hypothesis on the combiner). -/
def ledger_forces_regrouping
    (J : ℝ → ℝ) (hJ0 : J 1 = 0)
    (hSym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
    (P : ℝ → ℝ → ℝ)
    (hComp : ∀ x y : ℝ, 0 < x → 0 < y →
      J (x * y) + J (x / y) = P (J x) (J y))
    (hSurj : ∀ a : ℝ, ∃ x : ℝ, 0 < x ∧ J x = a)
    (hAffine : ∀ u, ∃ α β, ∀ v, P u v = α * v + β)
    (hP11 : P 1 1 = 6) :
    RegroupingInvariance J :=
  { combiner := P
    factors := hComp
    symmetric := combiner_symmetric J hSym P hComp hSurj
    zero_boundary := combiner_zero_boundary J hJ0 P hComp hSurj
    unit_diagonal := hP11
    right_affine := hAffine }

What this page does not claim

Not every comparison system satisfies regrouping invariance; the theorem only applies to systems that do. The theorem does not prove that the cost function J itself is unique. The right-affine condition is not derived from the primitive properties within the machine-checked library.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DAlembert/LedgerFactorization.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: