proof

P42 Continuity criteria disagree

Lean spine source

Declarations: P42_continuity_criteria_can_disagree

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P42_continuity_criteria_can_disagree :
    ∃ x y : Bool, ToyMemoryContinuous x y ∧ ¬ ToyBodyContinuous x y :=
  ⟨true, false, trivial, by decide⟩

/-- C-LIMIT (P44, amended): technical invariants do not determine legitimacy.
    There is a technically-invariant change accepted by one legitimacy ordering
    and rejected by another. (Not the inconsistent `L c ∧ ¬ L c`.) -/