`Phase`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.ChurchTuringPhysicsStructure
domain: Information
line: 46 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Information.ChurchTuringPhysicsStructure on GitHub at line 46.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  43/-! ## I. The 8-Tick Phase Space is Finite -/
  44
  45/-- The 8-tick phase space: phases 0 through 7. -/
  46abbrev Phase := Fin 8
  47
  48/-- The number of phases in one 8-tick cycle. -/
  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),

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.