Foundation Discrete Logic Realization

The Boolean carrier

Discrete logic realization is a test bed built from the simplest possible carrier: two truth values, true and false. The framework's library of formal theorems defines a comparison cost on these values: zero when two propositions are equal, one when they differ. This is the entire substrate. From that single rule, the library shows that the arithmetic of counting numbers emerges anyway, as a forced structure rather than a chosen one.

The classical background is Boolean algebra, named for George Boole, who in 1854 showed that logic could be written as algebra with two values. The standard operations are AND, OR, and NOT, and the familiar laws include commutativity (p AND q equals q AND p) and distributivity. The discrete realization here uses only the comparison cost, not the full Boolean operation set, and still recovers the Peano surface: the structure of the natural numbers with zero and successor.

In Recognition Science, the framework's library models a ledger, a discrete record of recognition events, and asks what structure is forced when recognition has a cost. The Boolean carrier is the first non-continuous test case for this universal forcing. The library defines a mapping from the free step orbit, the repeated application of a successor operation, into the Boolean values by parity: identity maps to false, one step to true, two steps back to false, and so on. This interpretation satisfies the definition of a logic realization.

The library proves two properties of this realization. First, it has a non-trivial identity-step shadow, meaning the identity and the step are genuinely distinct in this carrier. Second, and more striking, the forced arithmetic of the Boolean realization is equivalent to the forced arithmetic of every other realization. The theorem states that the Peano carrier of the Boolean realization is isomorphic to the Peano carrier of any logic realization. A two-value system, with only equality and distinction, produces the same counting structure as any richer carrier.

The consequence is that arithmetic does not require a rich substrate. The natural numbers with zero and successor appear as an invariant across all realizations, including the most impoverished two-value one. This is a derivation, not a measurement: the library proves the equivalence as a theorem. The Peano surface is not assumed; it is forced by the cost structure itself.

/-- Boolean comparison cost: zero for equality, one for distinction. -/
def boolCost (p q : Bool) : Nat :=
  if p = q then 0 else 1

/-- The discrete realization has a non-trivial identity-step shadow. -/
theorem bool_hasIdentityStep : boolRealization.hasIdentityStep :=
  LogicRealization.hasIdentityStep_of_nontrivial boolRealization

/-- Boolean realization has the same forced arithmetic as every realization. -/
noncomputable def bool_arithmetic_invariant (R : LogicRealization.{0, 0}) :
    (UniversalForcing.arithmeticOf boolRealization).peano.carrier
      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
  ArithmeticOf.equivOfInitial
    (UniversalForcing.arithmeticOf boolRealization) (UniversalForcing.arithmeticOf R)

/-- The Boolean realization's forced arithmetic has the Peano surface. -/
theorem bool_peano_surface :
    ArithmeticOf.PeanoSurface (UniversalForcing.arithmeticOf boolRealization) :=
  UniversalForcing.peano_surface boolRealization

What this page does not claim

The Boolean carrier is not claimed to be the physical substrate of reality. The library does not prove that Boolean algebra itself is forced, only that its comparison cost yields the same arithmetic. The equivalence theorem does not state that all realizations are identical, only that their forced arithmetic structures are isomorphic.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DiscreteLogicRealization.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: