`interpret_collapses`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject
domain: Foundation
line: 267 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject on GitHub at line 267.

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

formal source

 264
 265/-- Even though the carrier image collapses, the iteration object is the
 266full `LogicNat`. Concretely: the interpretation map is not injective. -/
 267theorem interpret_collapses :
 268    ¬ Function.Injective
 269      (StrictLogicRealization.interpret strictBooleanRealization) := by
 270  intro hinj
 271  have h0 :
 272      StrictLogicRealization.interpret strictBooleanRealization LogicNat.identity =
 273        Nat.bodd 0 := interpret_eq_parity _
 274  have h2 :
 275      StrictLogicRealization.interpret strictBooleanRealization
 276        (LogicNat.step (LogicNat.step LogicNat.identity)) =
 277          Nat.bodd 2 := interpret_eq_parity _
 278  have hbodd : (Nat.bodd 0 : Bool) = Nat.bodd 2 := by decide
 279  have hboth :
 280      StrictLogicRealization.interpret strictBooleanRealization LogicNat.identity =
 281        StrictLogicRealization.interpret strictBooleanRealization
 282          (LogicNat.step (LogicNat.step LogicNat.identity)) := by
 283    rw [h0, h2, hbodd]
 284  have hne : LogicNat.identity ≠ LogicNat.step (LogicNat.step LogicNat.identity) :=
 285    LogicNat.zero_ne_succ _
 286  exact hne (hinj hboth)
 287
 288/-- Despite the carrier collapse, the iteration object is itself a
 289natural-number object — the same one as in the continuous positive-ratio
 290realization. -/
 291def boolean_freeOrbit_isNNO :
 292    IsNaturalNumberObject
 293      (N := StrictLogicRealization.FreeOrbit strictBooleanRealization)
 294      LogicNat.identity LogicNat.step :=
 295  logicNat_isNNO
 296
 297end Strict.DiscreteBoolean

papers checked against this theorem

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