Foundation Recognition Time Delta

The recognition clock

Recognition time is the framework's internal clock. It is a discrete record of events, a sequence of ticks where each recognition step moves the clock forward by exactly one. The module RecognitionTimeDelta establishes that this clock is not a loose metaphor but a precise mathematical object: it proves that recognition time is a Peano model, meaning it has a zero, a successor function, and an induction principle, just like the counting numbers.

The central theorem is recognitionTime_isPeano, which shows that the structure of ticks and steps satisfies the Peano axioms. This is not an assumption; it is a proved result in the framework's machine-checked library of formal theorems. The library also proves that a single recognition step advances the clock by one, that appending to the ledger advances the clock by one, and that any formula forced by the empty ledger is true in recognition time. This means the framework's own logic and its model of time are consistent with each other.

For a finite observation, the module is careful not to overreach. It defines a finite prefix of ticks, from zero up to some bound n, and proves that this prefix agrees with the full clock on zero, successor, equality, and exact coverage. But it also proves that the last tick in any finite prefix has no successor within that prefix. A finite observation therefore receives only bounded agreement and is never promoted to a full Peano model. The unbounded theorem is about recognition time as a mathematical object, not about any particular laboratory device.

What this establishes in plain language is that the framework's notion of time is not ad hoc. It is a genuine arithmetic structure, the same structure that underlies counting and induction. This matters because it lets the framework carry theorems about its own logic into its model of time, and it sets a clear boundary: the mathematics is proved, while the identification of a specific physical device with this clock remains an external premise.

/-- Recognition time satisfies the Peano laws required by the δ transport
surface: successor is injective, zero is not a successor, and every tick is
generated from zero by repeated successor. -/
theorem recognitionTime_isPeano : IsPeanoModel recognitionTimeAlgebra where
  succ_injective := by
    intro a b h
    apply tickEquivNat.injective
    have hi : a.index + 1 = b.index + 1 := congrArg Tick.index h
    exact Nat.add_right_cancel hi
  zero_not_succ := by
    intro x h
    have hi := congrArg Tick.index h
    simp [recognitionTimeAlgebra, tickZero, tickSucc] at hi
  induction := by
    intro P hzero hsucc x
    cases x with
    | mk n =>
        induction n with
        | zero => exact hzero
        | succ n ih =>
            simpa [recognitionTimeAlgebra, tickSucc] using hsucc ⟨n⟩ ih

/-- A recognition transition is literally the successor map of the
recognition-time δ-algebra. -/
theorem recognition_step_is_delta_succ (step : RecognitionStep) :
    step.output.tick = recognitionTimeAlgebra.succ step.input.tick :=
  recognitionStep_iterates_succ step

/-- Appending one ledger entry is literally one δ successor on recognition
time. This is the concrete ledger-to-arithmetic commuting square. -/
theorem ledger_commit_is_delta_succ {E : Type*} (l : List E) (e : E) :
    ledgerTick (commit l e) = recognitionTimeAlgebra.succ (ledgerTick l) := by
  apply tickEquivNat.injective
  exact writeHead_advances l e

/-- Every empty-ledger δ theorem is true in RS recognition time. Transport adds
no premise and does not alter the checker ledger. -/
theorem forced_true_in_recognition_time {d : Deriv} {φ : DFormula}
    (h : Forced [] d φ) (ρ : Env) :
    msat recognitionTimeAlgebra ρ φ :=
  transport_forced h recognitionTimeAlgebra recognitionTime_isPeano ρ

/-- The terminal point has no in-prefix successor. This is the formal boundary
that blocks any claim that the finite carrier is a full Peano realization. -/
theorem prefixLast_not_in_succ_domain (n : Nat) :
    ¬ (prefixLast n).val < n := by
  simp [prefixLast]

What this page does not claim

No specific laboratory device is identified with the recognition clock. A finite observation is not promoted to a full Peano model. The framework's logic and its model of time are consistent, but this does not prove the framework's physical claims.

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