`StrictLogicRealization`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.StrictRealization
domain: Foundation
line: 26 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.StrictRealization on GitHub at line 26.

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

  23universe u v
  24
  25/-- A strict Law-of-Logic realization: native law data only, no supplied orbit. -/
  26structure StrictLogicRealization where
  27  Carrier : Type u
  28  Cost : Type v
  29  zeroCost : Zero Cost
  30  compare : Carrier → Carrier → Cost
  31  compose : Carrier → Carrier → Carrier
  32  one : Carrier
  33  generator : Carrier
  34  identity_law : ∀ x : Carrier, compare x x = 0
  35  non_contradiction_law : ∀ x y : Carrier, compare x y = compare y x
  36  excluded_middle_law : Prop
  37  composition_law : Prop
  38  invariance_law : Prop
  39  nontrivial_law : compare generator one ≠ 0
  40
  41attribute [instance] StrictLogicRealization.zeroCost
  42
  43namespace StrictLogicRealization
  44
  45/-- The strict free orbit is uniformly the `LogicNat` iteration object. -/
  46abbrev FreeOrbit (_R : StrictLogicRealization) : Type :=
  47  LogicNat
  48
  49/-- Interpret the free orbit of a strict realization in its carrier by
  50primitive recursion over the native generator and composition operation. -/
  51def interpret (R : StrictLogicRealization) : FreeOrbit R → R.Carrier
  52  | LogicNat.identity => R.one
  53  | LogicNat.step n => R.compose R.generator (interpret R n)
  54
  55@[simp] theorem interpret_zero (R : StrictLogicRealization) :
  56    interpret R LogicNat.zero = R.one := rfl

papers checked against this theorem

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