universal_forcing_via_NNO

formal source

 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
 251/-- The Boolean strict-realization interpretation is the parity map.
 252
 253This is the formal statement that the iteration count survives even when
 254the orbit-as-set collapses to `{false, true}`. -/
 255theorem interpret_eq_parity (n : LogicNat) :
 256    StrictLogicRealization.interpret strictBooleanRealization n =
 257      Nat.bodd (LogicNat.toNat n) := by