phase_space_finite

formal source

  49def numPhases : ℕ := 8
  50
  51/-- **THEOREM IC-003.1**: The 8-tick phase space has exactly 8 elements. -/
  52theorem phase_space_finite : Fintype.card Phase = 8 := by
  53  simp [Phase]
  54
  55/-- **THEOREM IC-003.2**: There are finitely many functions on the 8-tick phase space.
  56    |Phase → Phase| = 8^8 = 16,777,216 — a large but finite number. -/
  57theorem phase_functions_finite : Fintype.card (Phase → Phase) = 8 ^ 8 := by
  58  simp [Phase]
  59
  60/-! ## II. Ledger Transitions are Computable -/
  61
  62/-- A discrete ledger state: a function from phase indices to Bool values
  63    (representing whether each phase is "active"). -/
  64def DiscreteLedgerState := Fin 8 → Bool
  65deriving Fintype, DecidableEq
  66
  67/-- A ledger transition: a computable function on discrete states. -/
  68def LedgerTransition := DiscreteLedgerState → DiscreteLedgerState
  69
  70/-- **THEOREM IC-003.3**: Any ledger transition on the 8-tick phase space is
  71    a function on a finite type, hence computable by table lookup.
  72    Since there are only 2^8 = 256 possible discrete ledger states, any
  73    transition function can be pre-computed as a finite lookup table. -/
  74theorem discrete_ledger_computable (t : LedgerTransition) :
  75    ∃ (table : Finset (DiscreteLedgerState × DiscreteLedgerState)),
  76      ∀ (s : DiscreteLedgerState),
  77        ∃ (s' : DiscreteLedgerState), (s, s') ∈ table ∧ t s = s' := by
  78  use Finset.image (fun s => (s, t s)) Finset.univ
  79  intro s
  80  exact ⟨t s, Finset.mem_image.mpr ⟨s, Finset.mem_univ s, rfl⟩, rfl⟩
  81
  82/-- The number of possible discrete ledger states. -/