`strictNarrativeRealization`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.Narrative
domain: Foundation
line: 41 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.Strict.Narrative on GitHub at line 41.

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

  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

papers checked against this theorem

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