Foundation Pair Kernel Physical Valuation Initiality S19 Canonical Kinematics Op

The canonical duration readout

In the Recognition Science framework, a ledger is a discrete record of recognition events. The framework's library, a machine-checked collection of formal theorems, asks how such a record can assign physical properties like duration and energy to the events it logs. The declaration canonicalKinematics_operationalTickCount_model is a theorem in that library. It proves that for the framework's canonical model, the duration of an event is exactly the number of ticks, its discrete time steps, between the event's start and end.

This is not a choice made by hand. The theorem shows that a specific, natural construction, the canonical kinematics, satisfies the property of reading duration as an operational tick count. A separate theorem, recognitionTickCount_unique, proves that any real-valued function on ticks that starts at zero and adds one for each successor step must be the standard tick count. Together, these results mean that once you fix the scale of a single tick, the duration of any event is forced: it is the integer difference in tick counts, with no additional freedom to stretch or compress time.

The proof also shows what this model does not decide. A central theorem, no_weak_valuation_selects_absolute_scales, proves that the framework's basic rules do not pick out absolute units for duration or energy. Two different valuations can describe the same recognition data yet assign different scales to a single tick and a unit of energy. The canonical model fixes the combinatorics, the dimensionless ratios between durations, but the translation to seconds or joules remains an external calibration, not a consequence of the framework's axioms.

This distinction matters. The theorem canonicalKinematics_operationalTickCount_model is a precise statement about one model inside the framework. It does not claim that the framework derives the second or the joule from first principles. It does not claim that the operational tick count is the only possible way to read duration. It establishes a clean, provable relationship: in the canonical model, duration is a count, and that count is unique up to the choice of a single positive scale.

/-- MODEL witness only: the canonical kinematics reads the unit Tick count.
The theorem proves consistency, not physical selection. -/
theorem canonicalKinematics_operationalTickCount_model :
    PostingDurationReadsOperationalTickCount3
      (canonicalCoherenceKinematics3 3) := by
  intro event
  calc
    (canonicalCoherenceKinematics3 3).duration event.1 =
        1 := by
      simp [canonicalCoherenceKinematics3]
    _ = recognitionTickCount
          (postingEventEndTick3 event) -
        recognitionTickCount
          (postingEventStartTick3 3) := by
      rw [postingEventEndTick3_eq_succ]
      simp [recognitionTickCount, tickSucc]

/-- NNO initiality uniquely selects the dimensionless zero/successor-count
map. This theorem fixes a count, not a physical time unit. -/
theorem recognitionTickCount_unique
    (clock : Tick → ℝ)
    (hzero : clock tickZero = 0)
    (hsucc :
      ∀ tick : Tick,
        clock (tickSucc tick) = clock tick + 1) :
    clock = recognitionTickCount := by
  funext tick
  have hunique :=
    tick_isNNO.recursor_unique
      (0 : ℝ) (fun value => value + 1)
      clock hzero hsucc tick
  calc
    clock tick =
        tickRecursor (0 : ℝ)
          (fun value => value + 1) tick :=
      hunique
    _ = recognitionTickCount tick :=
      tickRecursor_real_succ_eq_count tick

/-- No inhabitant of the weak structural signature has absolute-scale
uniqueness. Scaling duration by two preserves every Recognition datum but
changes the positive one-successor unit. -/
theorem no_weak_valuation_selects_absolute_scales
    {N : ℕ} [NeZero N]
    (valuation : RecognitionPhysicalValuation3 N) :
    ¬ RecognitionDataSelectsAbsoluteScales3 valuation := by
  intro hselect
  let scaled :=
    scalePhysicalValuation3
      2 1 (by norm_num) (by norm_num) valuation
  have hsame : SameRecognitionData3 valuation scaled :=
    scalePhysicalValuation_sameRecognitionData
      2 1 (by norm_num) (by norm_num) valuation
  have hscales := (hselect scaled hsame).1
  change
    valuation.span.measure 1 =
      2 * valuation.span.measure 1 at hscales
  nlinarith [valuation.span_unit_pos]

What this page does not claim

The framework derives the SI second or the joule from its axioms. The canonical model is the only model in the framework that can assign durations to events. The theorem proves that the operational tick count is the correct physical readout, which remains a hypothesis.

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