Foundation Recognition Time Delta Bounded Ledger Tick Has Unique Address

The unique address

In the Recognition Science framework, a ledger is a discrete record of events, and each event occupies a tick, a numbered position in that record. The declaration bounded_ledger_tick_has_unique_address proves a simple but load-bearing fact: if you look at any finite prefix of the ledger, the tick at the write head, the position where the next event will be recorded, has exactly one address inside that prefix. No two addresses point to the same tick, and every tick in range has an address. This is the framework's way of saying that a finite observation of a ledger never loses track of where it is.

The proof works by showing that the set of addresses in a prefix of length n is exactly the set of ticks whose index is at most n. Since the mapping from addresses to ticks is injective, meaning distinct addresses give distinct ticks, the tick at the write head must correspond to one and only one address. The framework's machine-checked library of formal theorems verifies this reasoning from its axioms, with no hidden assumptions about the nature of the ledger or the observer.

This uniqueness result is what lets the framework treat a finite observation as a faithful window onto recognition time. A device that reads the ledger up to some bound can be certain that the tick it sees is the tick it means, not a stand-in or a duplicate. The theorem also certifies that the finite prefix agrees with the unbounded model on zero, successor, and equality, so a bounded observation is not a distorted picture of the whole, just a partial one.

The theorem does not claim that any particular physical device realizes the ledger or its tick readout. That identification remains an external premise, a matter of experiment, not proof. It also does not promote a finite observation to a full model of arithmetic: the last tick in a finite prefix has no successor inside the prefix, so the finite structure is deliberately partial. The uniqueness result is about the mathematics of the framework, not about any specific laboratory apparatus.

/-- Any append-only ledger whose write head is at most `n` has a unique address
inside the `n`-prefix. -/
theorem bounded_ledger_tick_has_unique_address {E : Type*} (n : Nat)
    (l : List E) (h : writeHead l ≤ n) :
    ∃! i : RecognitionPrefix n, prefixToTick i = ledgerTick l := by
  have hex : ∃ i : RecognitionPrefix n, prefixToTick i = ledgerTick l :=
    (tick_in_prefix_iff (n := n) (ledgerTick l)).mpr h
  obtain ⟨i, hi⟩ := hex
  refine ⟨i, hi, ?_⟩
  intro j hj
  exact prefixToTick_injective n (hj.trans hi.symm)

/-- Equality of finite observations reflects equality of recognition ticks. -/
theorem prefixToTick_injective (n : Nat) :
    Function.Injective (@prefixToTick n) := by
  intro i j h
  apply Fin.ext
  exact congrArg Tick.index h

/-- Every finite initial segment of recognition time has exact bounded
δ-agreement with the unbounded recognition-time realization. -/
theorem recognitionPrefix_agrees (n : Nat) : BoundedDeltaAgreement n where
  zero_preserved := rfl
  successor_preserved := prefixToTick_succ
  identity_reflected := prefixToTick_injective n
  successor_injective := by
    intro i j hi hj h
    exact prefixSucc_injective (i := i) (j := j) hi hj h
  zero_not_successor := prefixZero_not_succ
  exact_coverage := tick_in_prefix_iff
  terminal_is_boundary := prefixLast_not_in_succ_domain n

What this page does not claim

No particular laboratory device is identified with the ledger or its tick readout. A finite observation is not promoted to a full Peano model of arithmetic. The theorem does not say that the write head is the only tick with a unique address.

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: