Boolean Flip Has No Fixed Point

Abstract

The canonical exchange of the two Boolean statuses has no fixed point.

Theorem 1.1 (Boolean flip has no fixed point).

$\neg\exists s t a t u s : B oo l, s t a t u s = b oo lFl i p (s t a t u s) .$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GovernanceFixedPoint/BooleanFlipNoFixedPoint.bool_flip_has_no_fixed_point (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Boolean carrier has exactly the statuses false and true, and boolFlip exchanges them.

Constructor analysis therefore contradicts either proposed fixed-point equation without asserting anything about arbitrary non-blind derivers.

Truth anchor: D5/S3/ConceptDynamics/GovernanceFixedPoint/BooleanFlipNoFixedPoint.bool_flip_has_no_fixed_point
Dependency: D5/S3/ConceptDynamics/GovernanceFixedPoint/Core