Foundation Ledger Canonicality Admissible Cost

The Admissible Cost

A cost function assigns a number to every comparison: how expensive is it to recognize one state from another? The Recognition Science framework begins with a discrete record of events, its ledger, and asks what shape such a cost must take. The declaration AdmissibleCost pins down the answer by listing five properties any such cost must have. It requires reciprocal symmetry, meaning comparing x to y costs the same as comparing y to x; unit normalization, so comparing a state to itself costs zero; strict convexity, so costs rise faster than linearly; continuity; and a calibration condition that fixes the scale of curvature at the neutral point. These are not arbitrary choices: they are the minimal axioms a ledger needs to be a ledger at all.

The power of this definition is that it is not just a description. A separate theorem, proved in the machine-checked library of formal theorems, shows that any function satisfying these five conditions must equal J(x) = (x + 1/x)/2 - 1. The cost is forced, not chosen. This uniqueness result is the foundation on which the framework builds its later claims: the golden ratio, the eight-tick cycle, and the number of spatial dimensions all derive from this single functional form. The declaration itself, however, does not prove that theorem. It only defines the class of admissible costs, leaving the uniqueness result to the theorem that follows.

What the declaration does not claim is equally important. It does not assert that any particular cost function exists, only that if one exists it must have this form. It does not define conservation of charge; that is a separate structure that requires a transition map to state what is conserved over time. The declaration also does not specify how events compose at multiple scales. Composition is handled by later classes that build on this foundation. The definition is deliberately minimal, a single interface that downstream theorems can consume without worrying about which specific cost function they are using.

In Recognition Science, this declaration is the first step in a chain that ends with physical constants and the structure of space itself. But it earns that position precisely by being modest. It defines a class of functions, proves nothing about them, and leaves the heavy lifting to the theorems that follow. A reader who wants to know what the framework proves, rather than what it assumes, should look past this definition to the uniqueness theorem that gives the cost its power.

/-- A comparison cost on positive reals satisfying the minimal ledger
axioms: reciprocal symmetry, unit normalization, strict convexity,
continuity, and calibration. -/
structure AdmissibleCost where
  J : ℝ → ℝ
  reciprocal_sym : ∀ x : ℝ, 0 < x → J x = J (x⁻¹)
  unit_norm : J 1 = 0
  strict_convex : StrictConvexOn ℝ (Set.Ioi 0) J
  continuous : ContinuousOn J (Set.Ioi 0)
  calibration : (deriv (deriv (fun t => J (Real.exp t)))) 0 = 1

/-- A comparison cost on positive reals satisfying the minimal ledger
axioms: reciprocal symmetry, unit normalization, strict convexity,
continuity, and calibration. -/
structure AdmissibleCost where
  J : ℝ → ℝ
  reciprocal_sym : ∀ x : ℝ, 0 < x → J x = J (x⁻¹)
  unit_norm : J 1 = 0
  strict_convex : StrictConvexOn ℝ (Set.Ioi 0) J
  continuous : ContinuousOn J (Set.Ioi 0)
  calibration : (deriv (deriv (fun t => J (Real.exp t)))) 0 = 1

/-- A ledger scalar quantity on a type `α` with values in `ℝ`.

Conservation under dynamics is not a property of a bare charge function: it
requires a transition map (see `ClosedFramework.ClosedObservableFramework`,
field `charge_conserved : ∀ s, charge (T s) = charge s`). Former field
`charge_conserved : ∀ s₁ s₂, charge s₁ = charge s₂ → True` deleted (Move A):
equal charges implying `True` excluded nothing. -/
structure ConservedCharge (α : Type) where
  charge : α → ℝ

What this page does not claim

The AdmissibleCost declaration itself proves the uniqueness theorem; it only defines the class. The declaration specifies how events compose at multiple scales; that is handled by later classes. The declaration defines what it means for charge to be conserved over time.

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