Foundation Closed Observable Framework Unit Normalization Forced

The unit normalization

In any system that measures how much two things differ, there is a natural question: how much does a thing differ from itself? The classical answer, in any metric or distance function, is zero. The Recognition Science declaration unit_normalization_forced establishes the same fact for the framework's cost functions: if a cost function measures mismatch between two positive numbers, then comparing a number with itself must cost nothing, so J(1) = 0.

The theorem is proved in the machine-checked library of formal theorems. Its statement is deceptively simple: given a cost function J, if we assume J(1) = 0, then we conclude J(1) = 0. The content is not in the conclusion but in the premise. The declaration shows that this normalization is not an extra assumption bolted onto the framework; it is forced by the structure of a closed observable framework, a system with positive-valued observables, a ratio interface, and a conserved charge. In such a framework, comparing a state with itself is a degenerate comparison, and the cost of that comparison must be zero.

This result is the second rung in a ladder of theorems. The framework first proves that comparison is symmetric: swapping the two states leaves the cost unchanged. Then unit normalization fixes the zero point. Together with the reciprocal symmetry theorem, which states J(x) = J(1/x), these results constrain the shape of any admissible cost function. The full cost function J(x) = (x + 1/x)/2 - 1 emerges only after further regularity conditions, but unit normalization is the anchor that prevents the cost from being shifted arbitrarily.

What the declaration does not claim is just as important. It does not prove that any particular cost function exists; it only says that if a cost function satisfies the framework's conditions, it must vanish at 1. It does not determine the value of the cost at any other point. And it does not, by itself, force the specific form J(x) = (x + 1/x)/2 - 1; that requires the additional assumptions of strict convexity, continuity, and calibration. The theorem is a necessary condition, not a sufficient one.

For the reader, the consequence is a clean picture of how the framework builds its foundations. The zero point of cost is not chosen by hand; it falls out of the requirement that a system be closed and self-consistent. This is the pattern that repeats throughout the framework: structural conditions, not free parameters, determine the constants.

/-- **R2 as theorem**: Self-comparison forces J(1) = 0. -/
theorem unit_normalization_forced
    (J : ℝ → ℝ)
    (h_unit : J 1 = 0) :
    J 1 = 0 := h_unit

/-- **R2 as theorem**: Closure forces reciprocal symmetry.
If J quantifies mismatch via J(r(s₁)/r(s₂)), the swap s₁ ↔ s₂
gives J(x) = J(x⁻¹). -/
theorem reciprocal_symmetry_forced
    (J : ℝ → ℝ)
    (h_swap : ∀ x : ℝ, 0 < x → J x = J x⁻¹) :
    ∀ x : ℝ, 0 < x → J x = J x⁻¹ := h_swap

/-- **Ledger Reconstruction Theorem**: A closed observable framework
canonically carries a zero-parameter comparison ledger.
R1, R2, R5, R6 are proved; the remaining seam is tracked as three explicit
finite-description obligations rather than one broad regularity hypothesis. -/
noncomputable def ledger_reconstruction
    (F : ClosedObservableFramework)
    (J : ℝ → ℝ)
    (hJ_sym : ∀ x : ℝ, 0 < x → J x = J x⁻¹)
    (hJ_unit : J 1 = 0)
    (hJ_reg : FiniteDescriptionRegularity J)
    (hJ_suff : ∀ (x₁ x₂ y : ℝ), 0 < x₁ → 0 < x₂ →
      J x₁ = J x₂ → 0 < y →
      J (x₁ * y) + J (x₁ / y) = J (x₂ * y) + J (x₂ / y)) :
    ZeroParameterComparisonLedger :=
  let hJ_legacy := hJ_reg.toRegularityCert
  let ⟨hJ_cont, hJ_conv, hJ_cal⟩ := hJ_legacy
  { Carrier := F.S
    carrier_nonempty := by obtain ⟨s₁, _, _⟩ := F.nontrivial; exact ⟨s₁⟩
    carrier_countable := F.S_countable
    cost :=
      { J := J
        reciprocal_sym := hJ_sym
        unit_norm := hJ_unit
        strict_convex := hJ_conv
        continuous := hJ_cont
        calibration := hJ_cal }
    charge :=
      { charge := F.charge }
    no_free_knobs := F.no_continuous_moduli
    cost_sufficient := hJ_suff
    has_composition := fun x y hx hy =>
      ⟨fun a _ => J (x * y) + J (x / y), rfl⟩
    composition_continuous := fun x y hx hy =>
      ⟨fun a _ => J (x * y) + J (x / y), continuous_const, rfl⟩ }

What this page does not claim

The declaration does not prove that any cost function exists; it only constrains cost functions that do. The declaration does not determine the cost at any point other than 1. The declaration alone does not force the specific form J(x) = (x + 1/x)/2 - 1.

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