IndisputableMonolith.Foundation.UniversalForcing.Strict.Narrative

   1import IndisputableMonolith.Foundation.UniversalForcing.Strict.Biology
   2
   3/-!
   4  Strict/Narrative.lean
   5
   6  Domain-rich narrative realization over event states with act and beat
   7  coordinates. The generator is the inciting beat-step.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Foundation
  12namespace UniversalForcing
  13namespace Strict
  14namespace Narrative
  15
  16structure EventState where
  17  act : Nat
  18  beat : Nat
  19  deriving DecidableEq, Repr
  20
  21def eventCost (a b : EventState) : Nat :=
  22  if a = b then 0 else 1
  23
  24@[simp] theorem eventCost_self (a : EventState) : eventCost a a = 0 := by
  25  simp [eventCost]
  26
  27theorem eventCost_symm (a b : EventState) : eventCost a b = eventCost b a := by
  28  by_cases h : a = b
  29  · subst h
  30    simp [eventCost]
  31  · have h' : b ≠ a := by intro hb; exact h hb.symm
  32    simp [eventCost, h, h']
  33
  34def eventCompose (a b : EventState) : EventState :=
  35  { act := a.act + b.act, beat := a.beat + b.beat }
  36
  37def narrativeZero : EventState := ⟨0, 0⟩
  38def incitingBeat : EventState := ⟨0, 1⟩
  39
  40/-- Strict narrative realization using beat succession as the generator. -/
  41def strictNarrativeRealization : StrictLogicRealization where
  42  Carrier := EventState
  43  Cost := Nat
  44  zeroCost := inferInstance
  45  compare := eventCost
  46  compose := eventCompose
  47  one := narrativeZero
  48  generator := incitingBeat
  49  identity_law := eventCost_self
  50  non_contradiction_law := eventCost_symm
  51  excluded_middle_law := True
  52  composition_law := True
  53  invariance_law := True
  54  nontrivial_law := by
  55    simp [eventCost, incitingBeat, narrativeZero]
  56
  57def narrative_arith_equiv_logicNat :
  58    (StrictLogicRealization.arith strictNarrativeRealization).peano.carrier
  59      ≃ ArithmeticFromLogic.LogicNat :=
  60  (StrictLogicRealization.toLightweight strictNarrativeRealization).orbitEquivLogicNat
  61
  62end Narrative
  63end Strict
  64end UniversalForcing
  65end Foundation
  66end IndisputableMonolith
  67