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

papers checked against this theorem

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