boolRealization
The boolRealization assembles the discrete Boolean carrier for the Law-of-Logic structure, with Bool as the two-point set, natural numbers as costs, logical negation as the step, and the inductive LogicNat as the orbit. Researchers verifying that forced arithmetic is independent of carrier continuity cite this as the first non-continuous test case inside Universal Forcing. The definition populates the LogicRealization record by direct field assignment together with reflexivity proofs, the succ_injective theorem, and induction from ArithmeticOf.
claimThe discrete Boolean realization is the structure with carrier set the two-element Boolean algebra, cost set the natural numbers, zero element false, step operation logical negation, orbit the inductive type LogicNat generated by an identity constructor and a successor constructor, and interpretation map that preserves zero and successor.
background
LogicRealization is the record type that packages a carrier set, a cost function to natural numbers, a zero element, a step map, an orbit type, an interpretation map, and the axioms that the orbit satisfies the Peano properties forced by the Law of Logic. LogicNat is the inductive type whose constructors identity and step mirror the orbit {1, γ, γ², …} closed under multiplication by the generator γ; its zero and succ are the identity element and one further application of the generator. The module DiscreteLogicRealization supplies the second Law-of-Logic realization after the continuous case, serving as the first non-continuous test case for Universal Forcing.
proof idea
The definition constructs the LogicRealization record by assigning Carrier to Bool, Cost to Nat, compare to boolCost, zero to false, step to Bool.not, Orbit to LogicNat, and interpret to boolOrbitInterpret. The remaining fields are discharged by rfl for interpret_zero, interpret_step, orbitEquiv_zero and orbitEquiv_step; by zero_ne_succ for orbit_no_confusion; by succ_injective for orbit_step_injective; by the induction principle of LogicNat for orbit_induction; by Equiv.refl for orbitEquivLogicNat; and by boolCost_self, boolCost_symm together with a simple refinement for the identity, nonContradiction and nontrivial fields.
why it matters in Recognition Science
boolRealization is the concrete discrete realization exported by discreteRealization in UniversalForcing.DiscreteRealization and used to prove bool_arithmetic_invariant (arithmetic equivalence across realizations), bool_hasIdentityStep, and bool_peano_surface (the forced Peano surface). It supplies the first non-continuous test case for the Universal Forcing framework, confirming that the arithmetic extracted from any LogicRealization is isomorphic to the arithmetic forced by LogicNat. The definition therefore anchors the claim that the Peano surface is realization-independent before the forcing chain proceeds to T5–T8.
scope and limits
- Does not derive the forcing chain steps T0–T8 or J-uniqueness.
- Does not compute numerical values for constants such as α or G.
- Does not treat continuous carriers or the Recognition Composition Law.
- Does not address higher-dimensional or topological extensions of the orbit.
Lean usage
def discreteRealization : LogicRealization := boolRealizationformal statement (Lean)
34def boolRealization : LogicRealization where
35 Carrier := Bool
proof body
Definition body.
36 Cost := Nat
37 zeroCost := inferInstance
38 compare := boolCost
39 zero := false
40 step := Bool.not
41 Orbit := ArithmeticFromLogic.LogicNat
42 orbitZero := ArithmeticFromLogic.LogicNat.zero
43 orbitStep := ArithmeticFromLogic.LogicNat.succ
44 interpret := boolOrbitInterpret
45 interpret_zero := rfl
46 interpret_step := by intro n; rfl
47 orbit_no_confusion := by
48 intro n h
49 exact ArithmeticFromLogic.LogicNat.zero_ne_succ n h
50 orbit_step_injective := ArithmeticFromLogic.LogicNat.succ_injective
51 orbit_induction := by
52 intro P h0 hs n
53 exact ArithmeticFromLogic.LogicNat.induction (motive := P) h0 hs n
54 orbitEquivLogicNat := Equiv.refl ArithmeticFromLogic.LogicNat
55 orbitEquiv_zero := rfl
56 orbitEquiv_step := by intro n; rfl
57 identity := boolCost_self
58 nonContradiction := boolCost_symm
59 excludedMiddle := True
60 composition := True
61 actionInvariant := True
62 nontrivial := by
63 refine ⟨true, ?_⟩
64 simp [boolCost]
65
66/-- The discrete realization has a non-trivial identity-step shadow. -/