pith. machine review for the scientific record. sign in
theorem proved tactic proof

interpret_collapses

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 267theorem interpret_collapses :
 268    ¬ Function.Injective
 269      (StrictLogicRealization.interpret strictBooleanRealization) := by

proof body

Tactic-mode proof.

 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. -/

depends on (20)

Lean names referenced from this declaration's body.