IndisputableMonolith.Foundation.UniversalForcing.StrictRealization

   1import IndisputableMonolith.Foundation.UniversalForcing
   2
   3/-!
   4  StrictRealization.lean
   5
   6  Domain-rich Universal Forcing interface.
   7
   8  The earlier `LogicRealization` interface already proves the lightweight
   9  Universal Forcing theorem, but it lets a realization carry an internal orbit
  10  as a field.  `StrictLogicRealization` removes that escape hatch from the
  11  main theorem path: a strict realization supplies only native comparison,
  12  composition, identity, invariance, and non-triviality data.  The free orbit
  13  used by Universal Forcing is then derived uniformly as `LogicNat`.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace UniversalForcing
  19namespace Strict
  20
  21open ArithmeticFromLogic
  22
  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
  57
  58@[simp] theorem interpret_step (R : StrictLogicRealization) (n : FreeOrbit R) :
  59    interpret R (LogicNat.succ n) = R.compose R.generator (interpret R n) := rfl
  60
  61/-- Convert a strict realization to the existing lightweight interface.
  62The orbit fields are all derived from `LogicNat`, not supplied by the caller. -/
  63def toLightweight (R : StrictLogicRealization) : LogicRealization where
  64  Carrier := R.Carrier
  65  Cost := R.Cost
  66  zeroCost := R.zeroCost
  67  compare := R.compare
  68  zero := R.one
  69  step := fun x => R.compose R.generator x
  70  Orbit := FreeOrbit R
  71  orbitZero := LogicNat.zero
  72  orbitStep := LogicNat.succ
  73  interpret := interpret R
  74  interpret_zero := rfl
  75  interpret_step := by intro n; rfl
  76  orbit_no_confusion := by
  77    intro n h
  78    exact LogicNat.zero_ne_succ n h
  79  orbit_step_injective := LogicNat.succ_injective
  80  orbit_induction := by
  81    intro P h0 hs n
  82    exact LogicNat.induction (motive := P) h0 hs n
  83  orbitEquivLogicNat := Equiv.refl LogicNat
  84  orbitEquiv_zero := rfl
  85  orbitEquiv_step := by intro n; rfl
  86  identity := R.identity_law
  87  nonContradiction := R.non_contradiction_law
  88  excludedMiddle := R.excluded_middle_law
  89  composition := R.composition_law
  90  actionInvariant := R.invariance_law
  91  nontrivial := ⟨R.generator, R.nontrivial_law⟩
  92
  93/-- Strict forced arithmetic is the arithmetic extracted from the derived
  94lightweight realization. -/
  95def arith (R : StrictLogicRealization) : ArithmeticOf (toLightweight R) :=
  96  arithmeticOf (toLightweight R)
  97
  98/-- Every strict realization has forced arithmetic canonically equivalent to
  99`LogicNat`. -/
 100def arith_equiv_logicNat (R : StrictLogicRealization) :
 101    (arith R).peano.carrier ≃ LogicNat :=
 102  (toLightweight R).orbitEquivLogicNat
 103
 104/-- Universal forcing for strict realizations. -/
 105noncomputable def universal_forcing (R S : StrictLogicRealization) :
 106    (arith R).peano.carrier ≃ (arith S).peano.carrier :=
 107  ArithmeticOf.equivOfInitial (arith R) (arith S)
 108
 109/-- The Peano surface is inherited from the derived free orbit. -/
 110theorem peano_surface (R : StrictLogicRealization) :
 111    ArithmeticOf.PeanoSurface (arith R) :=
 112  UniversalForcing.peano_surface (toLightweight R)
 113
 114end StrictLogicRealization
 115
 116end Strict
 117end UniversalForcing
 118end Foundation
 119end IndisputableMonolith
 120