Foundation Substitutivity Forcing

Substitutivity from the ledger

Substitutivity is a property of a cost function: if two inputs have the same cost, then combining either one with a third input in the same way leaves the cost unchanged. In ordinary algebra, this is the kind of condition you might impose by hand. The framework's ledger, a discrete record of recognition events, carries a field named cost_sufficient that already encodes this rule. The first theorem, substitutivity_from_ledger, shows that for any positive x₁, x₂, and y, if J(x₁) = J(x₂), then J(x₁·y) + J(x₁/y) = J(x₂·y) + J(x₂/y). The proof is a direct use of the field; no new axiom is added.

The second part concerns calibration. The cost function J is part of the Aczél family cosh(λt), and the parameter λ must be fixed. The framework proves that λ = 1 is the unique positive real satisfying λ = λ⁻¹, meaning it is the only positive number that equals its own reciprocal. Since the framework's zero-parameter posture requires structural constants to have minimal descriptive complexity, and λ = 1 is the unique positive fixpoint of the inversion map, calibration is forced. The theorem calibration_forced_from_fixpoint states this directly: if λ is positive and λ = λ⁻¹, then λ = 1.

In plain terms, this work closes a gap in the framework's axiom-closure plan. It shows that two properties you might expect to be added as assumptions, substitutivity and calibration, are already consequences of the ledger structure. This is part of a larger effort to reduce the framework's axioms to zero, with each step verified by a machine-checked library of formal theorems.

/-- **Theorem (Substitutivity from Ledger)**: The `cost_sufficient`
field of `ZeroParameterComparisonLedger` directly provides contextual
substitutivity. No additional axiom needed. -/
theorem substitutivity_from_ledger
    (L : ZeroParameterComparisonLedger)
    (x₁ x₂ y : ℝ) (hx₁ : 0 < x₁) (hx₂ : 0 < x₂)
    (hJ_eq : L.cost.J x₁ = L.cost.J x₂) (hy : 0 < y) :
    L.cost.J (x₁ * y) + L.cost.J (x₁ / y) =
    L.cost.J (x₂ * y) + L.cost.J (x₂ / y) :=
  L.cost_sufficient x₁ x₂ y hx₁ hx₂ hJ_eq hy

/-- `λ = 1` is the unique positive real satisfying `λ = λ⁻¹`. -/
theorem lambda_one_is_unique_fixpoint :
    ∀ lam : ℝ, 0 < lam → lam = lam⁻¹ → lam = 1 := by
  intro lam hlam_pos hlam_eq
  have h1 : lam * lam = 1 := by
    have : lam * lam⁻¹ = 1 := mul_inv_cancel₀ (ne_of_gt hlam_pos)
    rw [← hlam_eq] at this; exact this
  nlinarith [sq_nonneg (lam - 1)]

/-- **Theorem**: Among the Aczél family cosh(λt), λ = 1 is the unique
positive real that equals its own reciprocal. Since the zero-parameter
posture requires all structural constants to have O(1) Kolmogorov
complexity, and λ = 1 is the unique positive fixpoint of the inversion
map, calibration is forced. -/
theorem calibration_forced_from_fixpoint
    (lam : ℝ) (hlam_pos : 0 < lam) (hlam_inv : lam = lam⁻¹) :
    lam = 1 :=
  lambda_one_is_unique_fixpoint lam hlam_pos hlam_inv

What this page does not claim

This work does not prove that the cost function J itself is unique; it only derives substitutivity and calibration from the ledger structure. The framework does not force the golden ratio or spatial dimensions; those results live in other parts of the framework.

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