interpret_eq_parity

formal source

 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
 258  induction n with
 259  | identity => rfl
 260  | step n ih =>
 261      show xorBool true (StrictLogicRealization.interpret strictBooleanRealization n) =
 262        Nat.bodd (Nat.succ (LogicNat.toNat n))
 263      rw [xorBool_true, ih, Nat.bodd_succ]
 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 _