strictBooleanRealization
The definition assembles the strict Boolean realization of the logic laws with carrier Bool and comparison cost that returns zero on equality and one on distinction. Researchers tracing discrete models in the forcing chain cite it to obtain the free iteration object LogicNat from propositional generators. The construction is a direct structure instantiation that wires in the Boolean cost lemmas and sets the excluded-middle and composition laws to True.
claimThe strict Boolean realization is the structure whose carrier is the set of Boolean values, whose cost function is the Boolean comparison cost (zero when arguments are equal, one otherwise), whose composition operation is exclusive-or, whose generator is true, and whose identity element is false.
background
StrictLogicRealization is the record type that packages a carrier set, a cost function to Nat, a composition operation, a generator, and the laws of logic (identity, non-contradiction, excluded middle, composition, invariance, nontriviality). The module supplies the strict discrete Boolean model in which the carrier orbit collapses to two points while the forced arithmetic remains the free iteration object. boolCost is the function that returns 0 on equal Booleans and 1 on distinct ones; boolCost_self and boolCost_symm are the lemmas establishing that this cost satisfies the identity and symmetry laws. LogicNat is the inductive type with constructors identity and step that encodes the orbit generated by repeated application of the generator.
proof idea
The definition is a direct structure instantiation. It assigns Bool to the carrier field, Nat to the cost field, boolCost to the compare field, xorBool to the compose field, false to the one field, and true to the generator field. The identity and non-contradiction laws are discharged by the lemmas boolCost_self and boolCost_symm; the remaining laws are supplied as the proposition True; the nontriviality law is proved by a single simp [boolCost] tactic.
why it matters in Recognition Science
This definition supplies the discrete Boolean model required by the NaturalNumberObject module. It is invoked to prove that the free orbit is an NNO (boolean_freeOrbit_isNNO), that the interpretation map collapses (interpret_collapses), and that the interpretation equals the parity map (interpret_eq_parity). The same definition appears in the cross-realization equivalence strictPositiveRatio_arith_equiv_strictBoolean, showing that positive-ratio and Boolean realizations force identical arithmetic. It therefore closes the discrete half of the invariance argument that links the strict forcing chain to LogicNat.
scope and limits
- Does not claim that the carrier set is infinite or that the interpretation map is injective.
- Does not construct a continuous embedding into the positive-ratio realization.
- Does not derive the mass formula or the value of the fine-structure constant.
- Does not address the Berry creation threshold or the dream fraction.
Lean usage
def exampleOrbit := StrictLogicRealization.FreeOrbit strictBooleanRealizationformal statement (Lean)
36def strictBooleanRealization : StrictLogicRealization where
37 Carrier := Bool
proof body
Definition body.
38 Cost := Nat
39 zeroCost := inferInstance
40 compare := boolCost
41 compose := xorBool
42 one := false
43 generator := true
44 identity_law := boolCost_self
45 non_contradiction_law := boolCost_symm
46 excluded_middle_law := True
47 composition_law := True
48 invariance_law := True
49 nontrivial_law := by
50 simp [boolCost]
51
52/-- Strict Boolean forced arithmetic is canonically `LogicNat`. -/