strictBooleanRealization
plain-language theorem explainer
The strict discrete Boolean realization equips the two-element set Bool with natural-number costs via boolCost and XOR composition to form a StrictLogicRealization. Researchers studying discrete models in the universal forcing chain cite it as the propositional base case. The definition directly assembles the carrier, cost, generator, and previously established cost lemmas into the required structure fields.
Claim. The strict Boolean realization is the instance of StrictLogicRealization whose carrier is the two-element Boolean algebra, whose cost function is the map returning 0 on equality and 1 on distinction, whose composition is XOR, whose identity element is false, whose generator is true, and whose laws are satisfied by the self-cost, symmetry, and trivial propositions for excluded middle, composition, and invariance.
background
The module introduces the strict Boolean realization in which the carrier collapses to two points while the forced arithmetic remains the free iteration object. Upstream, LogicNat is the inductive type with constructors identity (zero-cost element) and step (iteration of the generator), mirroring the orbit closed under multiplication by the generator and containing the identity. The comparison cost boolCost returns 0 when its arguments are equal and 1 otherwise; its self and symmetry properties are established by direct case analysis on equality.
proof idea
The definition instantiates the StrictLogicRealization structure by assigning Carrier to Bool, Cost to Nat, compare to boolCost, compose to xorBool, one to false, generator to true, identity_law to boolCost_self, non_contradiction_law to boolCost_symm, and the remaining laws to True, with the nontrivial_law discharged by a single simp tactic on boolCost.
why it matters
This supplies the discrete propositional model that feeds the NaturalNumberObject results, including boolean_freeOrbit_isNNO establishing that the free orbit is an NNO and interpret_eq_parity identifying the interpretation map with parity on LogicNat. It underpins the cross-realization invariance theorem showing that positive-ratio and Boolean realizations induce equivalent arithmetic, realizing the strict forcing step for the propositional case in the chain from LogicNat to the universal arithmetic object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.