strictBooleanRealization
plain-language theorem explainer
strictBooleanRealization supplies the Boolean carrier with Nat costs and XOR composition as an instance of StrictLogicRealization. Researchers on discrete logic-to-arithmetic forcing cite it to obtain the free orbit as LogicNat. The definition populates structure fields directly, discharging the sole nontrivial law by simplification on boolCost.
Claim. The strict discrete Boolean realization is the structure with carrier set Bool, cost function $c(p,q)=0$ if $p=q$ else $1$, composition the symmetric difference operation, distinguished elements false (identity) and true (generator), and proofs that these data satisfy the identity law, non-contradiction law, excluded-middle law, composition law, invariance law, and nontriviality law.
background
StrictLogicRealization is the record type whose fields are a carrier set, a cost function into Nat, a composition operation, distinguished one and generator elements, and proofs of the laws of logic (identity, non-contradiction, excluded middle, composition, invariance, nontriviality). boolCost is the function returning 0 on equal Booleans and 1 on distinct Booleans; its self and symm theorems establish reflexivity and symmetry. LogicNat is the inductive type 'The natural numbers as forced by the Law of Logic' whose constructors identity and step generate the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator and containing 1. The module places this definition inside the strict Boolean setting where the periodic carrier is separated from the free iteration object.
proof idea
The definition is a direct record construction that sets 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. The nontrivial_law is discharged by the tactic simp [boolCost]. All other fields are supplied by the upstream definitions boolCost, boolCost_self, and boolCost_symm.
why it matters
This supplies the Boolean instance required by boolean_freeOrbit_isNNO ('Despite the carrier collapse, the iteration object is itself a natural-number object') and by interpret_eq_parity (the interpretation map equals the parity function on LogicNat). It participates in the cross-realization equivalence strictPositiveRatio_arith_equiv_strictBoolean and in interpret_collapses showing the interpretation map fails to be injective. The construction therefore closes the discrete Boolean case of the forcing from logic to the natural-number object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.