Foundation Ledger Comparison To Composition

From comparison to composition

In Recognition Science, a framework that derives physical structure from the cost of recognition events, the ledger is a discrete record of observable states. The comparison between two states s₁ and s₂ is the ratio of their observables, r(s₁)/r(s₂). This ratio is always positive, swapping the states sends it to its reciprocal, and comparing a state to itself gives exactly 1. These three facts are not assumed; they are read off from the ledger's own structure.

The central question is what happens when you combine two comparisons. The framework asks whether the sum of two costs, F(x·y) + F(x/y), depends only on the individual costs F(x) and F(y), not on the particular ratios x and y that produced them. This condition is called being cost-determined. The development proves that this condition is exactly equivalent to the existence of a binary combiner P such that F(x·y) + F(x/y) = P(F(x), F(y)). In other words, the combiner is not an arbitrary analytic input; it exists precisely when the combination is a function of the costs alone.

This equivalence closes a gap in the framework's derivation. Earlier work had assumed the existence of such a combiner as a hypothesis. This development derives it from the ledger's own well-definedness condition. The result is a composite theorem: a comparison cost that is reciprocal, normalized, calibrated, and continuous, whose symmetric combination is realized through a primitive ledger-posting combiner with per-slice directional regularity, is forced to be J(x) = (x + 1/x)/2 - 1. The composition law follows from the ledger, not from an assumed analytic structure.

The development also shows the condition is not vacuous. The cost function J itself satisfies the cost-determined condition, since it composes through a specific combiner. The entire development is machine-checked, with zero axioms beyond the standard three and no unproved assumptions. This means the step from comparison to composition is a proved theorem, not a conjecture.

/-- The comparison ratio between two observable states of a closed framework. -/
noncomputable def compRatio (F : ClosedObservableFramework) (s₁ s₂ : F.S) : ℝ :=
  F.r s₁ / F.r s₂

/-- **Factorization existence ⇔ cost-determined combination.**  A comparison cost
admits a binary combiner `P` with `F(x·y) + F(x/y) = P(F x, F y)` (the d'Alembert
`HasMultiplicativeConsistency` factorization input) **iff** its symmetric
combination is cost-determined.  So the combiner is not an arbitrary analytic
assumption: it exists exactly when the combination is a function of the costs
alone.  The reverse direction builds `P` by choosing, for each cost pair in the
image, a witnessing ratio pair; cost-determinedness makes the choice irrelevant. -/
theorem hasMultiplicativeConsistency_iff_costDetermined (F : ℝ → ℝ) :
    DAlembert.Ultimate.HasMultiplicativeConsistency F ↔ CombinationCostDetermined F := by
  constructor
  · rintro ⟨P, hP⟩ x₁ y₁ x₂ y₂ hx₁ hy₁ hx₂ hy₂ hFx hFy
    rw [hP x₁ y₁ hx₁ hy₁, hP x₂ y₂ hx₂ hy₂, hFx, hFy]
  · intro hdet
    classical
    refine ⟨fun u v =>
      if h : ∃ p : ℝ × ℝ, 0 < p.1 ∧ 0 < p.2 ∧ F p.1 = u ∧ F p.2 = v
      then F (h.choose.1 * h.choose.2) + F (h.choose.1 / h.choose.2)
      else 0, ?_⟩
    intro x y hx hy
    have hex : ∃ p : ℝ × ℝ, 0 < p.1 ∧ 0 < p.2 ∧ F p.1 = F x ∧ F p.2 = F y :=
      ⟨(x, y), hx, hy, rfl, rfl⟩
    show F (x * y) + F (x / y) =
      (if h : ∃ p : ℝ × ℝ, 0 < p.1 ∧ 0 < p.2 ∧ F p.1 = F x ∧ F p.2 = F y
        then F (h.choose.1 * h.choose.2) + F (h.choose.1 / h.choose.2)
        else 0)
    rw [dif_pos hex]
    obtain ⟨hp1, hp2, hpx, hpy⟩ := hex.choose_spec
    exact (hdet hex.choose.1 hex.choose.2 x y hp1 hp2 hx hy hpx hpy).symm

/-- **Phase 3 composite.**  A comparison cost that is reciprocal, normalized,
calibrated, and continuous, whose symmetric combination is realized through a
primitive ledger-posting combiner with per-slice directional regularity, is forced
to be `J`.  The factorization combiner is supplied through the ledger (so it is
forced to `rclCombiner`), the composition law follows, and
`law_of_logic_forces_jcost` finishes, with no analytic composition-law hypothesis
assumed. -/
theorem ledgerComparison_forces_jcost
    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hRecip : IsReciprocalCost F) (hNorm : IsNormalized F)
    (hCalib : IsCalibrated F) (hCont : ContinuousOn F (Set.Ioi 0))
    (hP : LedgerToFactorization.PrimitiveLedgerPostingSemantics P)
    (hdir : ∀ u, Monotone (fun v => P u v) ∨ Antitone (fun v => P u v))
    (hCompose : CostComposesThrough F P) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
  ledgerComposition_forces_jcost F P hRecip hNorm hCalib hCont hP hdir hCompose

/-- **`J`'s combination is cost-determined.**  Since `J` composes through
`rclCombiner`, its symmetric combination is a function of the single-point costs,
so the factorization-existence condition is non-vacuous. -/
theorem jcost_combinationCostDetermined :
    CombinationCostDetermined Cost.Jcost :=
  (hasMultiplicativeConsistency_iff_costDetermined Cost.Jcost).mp
    ⟨rclCombiner, jcost_composesThrough_rclCombiner⟩

What this page does not claim

This does not claim that the composition law is derived without any regularity conditions. This does not claim that the cost-determined condition is the only way to derive the composition law. This does not claim that the ledger itself is derived from more primitive principles.

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/LedgerComparisonToComposition.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: