realizationOrbit_equiv_logicNat

formal source

 217/-- The forced arithmetic of every realization is canonically equivalent to
 218`LogicNat`. This is the Universal Forcing statement at the natural-number
 219object level: every Law-of-Logic realization carries the same NNO. -/
 220noncomputable def realizationOrbit_equiv_logicNat (R : LogicRealization.{0, 0}) :
 221    R.Orbit ≃ LogicNat :=
 222  IsNaturalNumberObject.equiv (realizationOrbit_isNNO R) logicNat_isNNO
 223
 224/-- The Lawvere universality statement: any two realizations have iteration
 225orbits that satisfy the natural-number-object property, hence are
 226canonically equivalent. -/
 227noncomputable def universal_forcing_via_NNO
 228    (R S : LogicRealization.{0, 0}) : R.Orbit ≃ S.Orbit :=
 229  IsNaturalNumberObject.equiv (realizationOrbit_isNNO R) (realizationOrbit_isNNO S)
 230
 231/-! ## The Boolean parity-collapse theorem
 232
 233The discrete Boolean realization is the sharpest test of the iteration-object
 234versus orbit-as-set distinction. The carrier `Bool` has only two elements,
 235and the strict realization's `interpret : LogicNat → Bool` collapses
 236infinitely many iteration steps onto two values. The iteration object
 237itself never collapses; it is `LogicNat`, the natural-number object.
 238
 239The theorem below makes the collapse explicit: the Boolean interpretation
 240is exactly the parity map `Nat.bodd ∘ toNat`. -/
 241
 242namespace Strict.DiscreteBoolean
 243
 244open IndisputableMonolith.Foundation.UniversalForcing.Strict
 245
 246/-- One step of the Boolean strict realization is `xor true _`, which is
 247boolean negation. -/
 248private theorem xorBool_true (b : Bool) : xorBool true b = !b := by
 249  cases b <;> rfl
 250