boolRealization
plain-language theorem explainer
boolRealization assembles the Boolean carrier for the discrete Law-of-Logic realization. Workers on discrete models of the forcing chain cite it as the first propositional test case. The definition populates the LogicRealization record by setting Carrier to Bool, Cost to Nat via boolCost, Orbit to LogicNat, and supplying the required maps and invariants directly from ArithmeticFromLogic.
Claim. The discrete propositional realization is the structure with carrier set $B = {0,1}$, cost function taking values in $ℕ$, zero element $0$, successor map the logical negation, orbit the inductive type $LogicNat$ generated by an identity element and a successor, and interpretation map sending the orbit to the carrier with the listed zero, step, and induction properties.
background
LogicRealization is the record type whose instances supply a carrier set, a cost function, a zero element, a step map, an orbit type, an interpretation map, and a collection of invariants including identity, non-contradiction, and arithmetic compatibility. LogicNat is the inductive type with constructors identity and step; its doc-comment states that identity represents the zero-cost element and step represents iteration of the generator, mirroring the orbit closed under multiplication by the generator. The module DiscreteLogicRealization supplies the second Law-of-Logic realization and is described as the first non-continuous test case for Universal Forcing. Upstream results include succ_injective and succ from ArithmeticFromLogic, which establish the Peano properties forced by the inductive structure of LogicNat.
proof idea
The definition directly assigns each field of the LogicRealization record. Carrier, Cost, zero, step, Orbit, orbitZero, orbitStep, interpret, interpret_zero, interpret_step, orbitEquivLogicNat, orbitEquiv_zero, orbitEquiv_step, excludedMiddle, composition, and actionInvariant receive literal or rfl assignments. orbit_no_confusion applies zero_ne_succ, orbit_step_injective applies succ_injective, orbit_induction applies the induction principle of LogicNat, nontrivial uses a concrete witness true together with simp on boolCost, and identity and nonContradiction cite the sibling lemmas boolCost_self and boolCost_symm.
why it matters
boolRealization is the concrete instance used to define discreteRealization in UniversalForcing.DiscreteRealization and to prove bool_arithmetic_invariant, bool_hasIdentityStep, and bool_peano_surface. The latter two establish that the forced arithmetic of this realization satisfies the Peano surface and possesses a non-trivial identity-step shadow. It supplies the discrete propositional test case required by the Universal Forcing module and therefore sits inside the forcing chain after the definition of LogicNat and before the arithmetic invariants that hold uniformly across realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.