LedgerTransition

formal source

  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. -/
  83def numLedgerStates : ℕ := 2 ^ 8
  84
  85/-- **THEOREM IC-003.4**: The discrete ledger state space is finite (exactly 2^8 = 256). -/
  86theorem ledger_state_space_finite :
  87    Fintype.card DiscreteLedgerState = 2 ^ 8 := by
  88  simp [DiscreteLedgerState, Fintype.card_pi, Fintype.card_fin, Fintype.card_bool]
  89
  90/-! ## III. RS Dynamics are Church-Turing Computable -/
  91
  92/-- Carrier of computation_limits_from_ledger through the chain. -/
  93theorem has_computation_limits_structure : computation_limits_from_ledger :=
  94  computation_limits_structure
  95
  96/-- The Church-Turing physics property: physical processes are computable. -/
  97def church_turing_physics_from_ledger : Prop := computation_limits_from_ledger
  98