Foundation Primitive Recognition Calculus Objecthood Registry Classify Conventio

The cost unit as a gauge

The declaration classify_convention is a formal statement about the unit used to measure cost in the Recognition Science framework. Cost here means the price of recognition, the quantity that a ledger, a discrete record of events, tracks. The theorem proves that this unit is a convention, a gauge or labeling choice, rather than something forced by the underlying mathematics. It is like the choice between measuring length in meters or feet: the physics does not change, only the numbers on the ruler.

The proof works with a specific family of cost functions, those of the form cosh(c*t) - 1, where c is a positive real number that sets the scale. The theorem establishes two facts. First, if two such functions with different scales c and d are identical for all times t, then c must equal d. The scale is not redundant; each value of c gives a genuinely different function. Second, and this is the key point, for any two positive scales c and d, there exists a positive number μ such that rescaling time by μ makes the two functions equal. In symbols: cosh(c*(μ*t)) - 1 = cosh(d*t) - 1. This means the difference between two scales is always absorbable into a change of the time unit. No experiment can distinguish between a cost function with scale c and one with scale d, because a simple relabeling of time makes them identical. The unit is therefore a pure convention, a free real parameter fixed only by a choice of measurement standard.

This result is part of a larger classification scheme, a periodic table of objecthood, that assigns every mathematical object in the framework a commitment type. The commitment types are: forced, meaning uniquely determined by the law; permitted, meaning an admissible free choice; quotient, meaning an identification under an equivalence; completion, meaning closure adding limit points; display, meaning a rendering instrument; observable, meaning defined by what can be measured; and convention, meaning a gauge or labeling choice. The theorem classify_convention is the evidence that the cost-scale unit gets the convention tag. Other objects get different tags: the rational numbers are forced into every carrier, the real numbers require completion, and the physical quotient is forced by indistinguishability.

What the declaration does not claim is just as important. It does not say that the cost function itself is a convention. The function J(x) = (x + 1/x)/2 - 1 is forced by the five plain conditions; that is a separate theorem. The convention is only about the unit, the scale c in the cosh family, not about the shape of the cost law. The declaration also does not claim that all units in physics are conventions. It speaks only to the cost-scale unit within this framework. Finally, it does not claim that the choice of unit has no effect at all. The theorem shows the effect is a pure rescaling of time, which is exactly what a gauge choice should be: it changes the labels, not the physics.

The practical upshot is that the framework is honest about what it does and does not determine. It forces the form of the cost function, but it leaves the unit as a free choice, a gauge. This is not a weakness; it is a precise statement of what a measurement standard is. The reader can now see that the framework distinguishes sharply between what is mathematically necessary and what is a matter of convention, and that this distinction is itself proved, not assumed.

/-- `convention`: the cost-scale unit is a faithful, transitively-rescaled torsor,
a single free real fixed only by a continuum-side datum. It is a gauge. -/
theorem classify_convention :
    (∀ c d : ℝ, 0 < c → 0 < d →
        (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d)
      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
          ∃ μ : ℝ, 0 < μ ∧
            (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1)) :=
  DeltaRealCalibration.discrete_does_not_force_unit

/-- `convention`: the cost-scale unit is a faithful, transitively-rescaled torsor,
a single free real fixed only by a continuum-side datum. It is a gauge. -/
theorem classify_convention :
    (∀ c d : ℝ, 0 < c → 0 < d →
        (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d)
      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
          ∃ μ : ℝ, 0 < μ ∧
            (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1)) :=
  DeltaRealCalibration.discrete_does_not_force_unit

/-- **Phase 8 headline: the periodic table of objecthood.** Each catalogued object
carries its commitment, and the assignment is exactly the evidence above:
distinction-forced (rationals, the coherence scale), display (ℝδ value map),
completion (ℝ), convention (cost unit), quotient and observable (the gauge
quotient and its probes), permitted (the generable inventory). Objecthood is not
flat: each object is produced by a specific kind of commitment, and the kind is
now a typed, proved attribute. -/
theorem objecthood_periodic_table :
    commitmentOf RSObject.deltaRationals = Commitment.forced
      ∧ commitmentOf RSObject.protocolReals = Commitment.display
      ∧ commitmentOf RSObject.classicalReals = Commitment.completion
      ∧ commitmentOf RSObject.calibrationUnit = Commitment.convention
      ∧ commitmentOf RSObject.physicalQuotient = Commitment.quotient
      ∧ commitmentOf RSObject.observableFamily = Commitment.observable
      ∧ commitmentOf RSObject.generableCarrier = Commitment.permitted
      ∧ commitmentOf RSObject.primeScale = Commitment.forced :=
  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩

What this page does not claim

The cost function itself is not a convention; its form is forced by the five plain conditions. The declaration does not claim that all units in physics are conventions, only the cost-scale unit within this framework. The choice of unit has no effect at all; the theorem shows the effect is a pure rescaling of 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/PrimitiveRecognitionCalculus/ObjecthoodRegistry.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: