Foundation Dalembert Ledger Factorization

Ledger factorization

The d'Alembert equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, is the classical wave equation. In one dimension it reads ∂²u/∂t² = c²∂²u/∂x², and its general solution is the sum of a left-moving and a right-moving wave. This factorization of the solution into two traveling waves is the classical meaning of the term.

In Recognition Science, the same word names a different but structurally parallel factorization. The framework begins with a ledger, a discrete record of comparison events, where each event assigns a cost, a number measuring mismatch between two quantities. The central question is how to combine two such costs into one. The module proves that two plain properties of the ledger force the combining rule to have a single exact form.

The first property is contextual substitutivity: if two subcomparisons carry the same mismatch cost, they are interchangeable in any larger comparison. The compound cost of a pair (x, y) depends only on the individual costs J(x) and J(y), not on the specific values of x and y. The second is regrouping invariance: the cost of comparing three quantities does not depend on how the comparisons are parenthesized. The combiner P must be symmetric, must satisfy boundary conditions, and must respond affinely to each argument.

From these two properties, the machine-checked library of formal theorems derives the factorization: the combiner must be P(u,v) = 2uv + 2u + 2v. This is the Recognition Composition Law. The proof runs through an associativity gate, a technical intermediate structure, and the key theorem is named ledger_forces_rcl. The result is unconditional: no extra hypotheses beyond the two ledger properties are needed.

What this establishes in plain language is that the ledger's combination rule is not a choice. If a comparison ledger treats equal-cost subcomparisons as interchangeable, and if regrouping comparisons does not change the total cost, then the way costs combine is forced. This factorization is the bridge from the ledger's primitive structure to the functional equation that determines the cost function J itself.

/-- **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)

/-- Contextual substitutivity: the compound cost of a pair `(x, y)`
depends only on `J(x)` and `J(y)`, not on the specific values of
`x` and `y`.  This is the minimal invariance principle of a
comparison ledger: if two subcomparisons carry the same mismatch
cost, they are interchangeable in any compound context. -/
structure ContextualSubstitutivity (J : ℝ → ℝ) where
  combiner : ℝ → ℝ → ℝ
  factors : ∀ x y : ℝ, 0 < x → 0 < y →
    J (x * y) + J (x / y) = combiner (J x) (J y)

/-- Regrouping invariance: the combiner is symmetric and satisfies the
boundary and normalization conditions forced by the abelian group
structure of `(ℝ₊, ×)` and the calibration of `J`. -/
structure RegroupingInvariance (J : ℝ → ℝ) extends ContextualSubstitutivity J where
  symmetric : ∀ u v, combiner u v = combiner v u
  zero_boundary : ∀ u, combiner u 0 = 2 * u
  unit_diagonal : combiner 1 1 = 6
  right_affine : ∀ u, ∃ α β, ∀ v, combiner u v = α * v + β

What this page does not claim

This answer does not claim that contextual substitutivity alone forces the combiner; regrouping invariance is also required. This answer does not claim that the classical d'Alembert wave equation is derived from the ledger; the shared name is an analogy. This answer does not claim that the right-affine response of the combiner is proved from the ledger properties; it is encoded as a hypothesis in the module.

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: