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. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.