IndisputableMonolith.Foundation.LedgerTime

   1import Mathlib
   2
   3/-!
   4# LedgerTime: the append-only structure of recognition time
   5
   6The bare recognition tick is invertible, hence time-symmetric. The lived asymmetry
   7between a fixed, readable past and an open, widening future is not in the tick; it
   8enters with the **ledger**: the append-only record of committed recognition events.
   9
  10This module formalizes that structure abstractly over an entry type `E`:
  11
  12* `commit` appends a new entry (append-only, never edits in place);
  13* the **committed past** is immutable and addressable under a new commit
  14  (`past_immutable`, `past_addressable`), and the write-head advances by exactly
  15  one (`writeHead_advances`);
  16* the **admissible future cone** never shrinks (`cone_grows`,
  17  `cone_card_monotone`): the count of admissible continuations is nondecreasing in
  18  horizon.
  19
  20Status: THEOREM for the structural facts (these are standard list/finset lemmas).
  21MODEL for the identification of `E` with recognition entries and of `coneStep`
  22with the J-admissible continuation set; that identification is argued in the
  23companion paper, not here.
  24-/
  25
  26namespace IndisputableMonolith
  27namespace Foundation
  28namespace LedgerTime
  29
  30variable {E : Type*}
  31
  32/-- Commit a new entry to the ledger: append-only. -/
  33def commit (l : List E) (e : E) : List E := l ++ [e]
  34
  35/-- The write-head index (the present): the number of committed entries. -/
  36def writeHead (l : List E) : ℕ := l.length
  37
  38/-- **Past immutability.** Truncating the extended ledger back to the old length
  39returns the old ledger exactly: committing a new entry cannot alter the past.
  40
  41Strategy: `unfold commit; exact List.take_left l [e]` (or
  42`simp [commit, List.take_left]`). -/
  43theorem past_immutable (l : List E) (e : E) :
  44    (commit l e).take l.length = l := by
  45  unfold commit; simp
  46
  47/-- **Write-head advance.** The present index moves forward by exactly one per
  48commit.
  49
  50Strategy: `simp [writeHead, commit, List.length_append]`. -/
  51theorem writeHead_advances (l : List E) (e : E) :
  52    writeHead (commit l e) = writeHead l + 1 := by
  53  unfold writeHead commit; simp
  54
  55/-- **Past addressability.** Every committed past index reads the same value after
  56a new commit: the past is read-only and addressable by index.
  57
  58Strategy: `unfold commit; exact List.getElem?_append_left hi` (find the exact
  59`getElem?_append` lemma for the index-in-left-segment case via the premises). -/
  60theorem past_addressable (l : List E) (e : E) (i : ℕ) (hi : i < l.length) :
  61    (commit l e)[i]? = l[i]? := by
  62  unfold commit; rw [List.getElem?_append_left hi]
  63
  64variable [DecidableEq E]
  65
  66/-- One step of the admissible future cone: the current frontier together with all
  67its admissible successors under `next`. -/
  68def coneStep (next : E → Finset E) (S : Finset E) : Finset E :=
  69  S ∪ S.biUnion next
  70
  71/-- **The cone never shrinks.** The frontier is contained in its successor cone.
  72
  73Strategy: `unfold coneStep; exact Finset.subset_union_left`. -/
  74theorem cone_grows (next : E → Finset E) (S : Finset E) :
  75    S ⊆ coneStep next S := by
  76  unfold coneStep; exact Finset.subset_union_left
  77
  78/-- **Admissible count nondecreasing.** The number of admissible states is
  79nondecreasing in horizon.
  80
  81Strategy: `exact Finset.card_le_card (cone_grows next S)`. -/
  82theorem cone_card_monotone (next : E → Finset E) (S : Finset E) :
  83    S.card ≤ (coneStep next S).card := by
  84  exact Finset.card_le_card (cone_grows next S)
  85
  86end LedgerTime
  87end Foundation
  88end IndisputableMonolith
  89