Foundation Universal Forcing Strict Discrete Boolean

Strict Boolean arithmetic

In classical logic, a proposition is either true or false. Recognition Science asks what arithmetic structure emerges when a ledger, a discrete record of events, is built from just these two truth values. The answer, proved in the framework's machine-checked library of formal theorems, is that the strict Boolean realization forces the same arithmetic as the positive real numbers. The module Strict/DiscreteBoolean.lean establishes this by defining a cost function on pairs of Booleans: the cost is 0 when the two values agree, and 1 when they differ. This is the simplest possible symmetric cost, yet it generates a carrier orbit that is periodic, not infinite.

The key move is to distinguish the finite Boolean image from the arithmetic it forces. The cost function alone, applied to two Booleans, gives a periodic structure. But the strict forced arithmetic, derived from the native generator of the realization, is not that finite image. Instead, it is canonically equivalent to LogicNat, the framework's natural-number object built from logic itself. The theorem strictBoolean_arith_equiv_logicNat states this equivalence explicitly: the Peano carrier of the strict Boolean arithmetic is isomorphic to LogicNat. This is not a definitional choice; it is a proved structural identity.

The module then proves a stronger invariance result. The theorem strictPositiveRatio_arith_equiv_strictBoolean shows that the arithmetic forced by positive ratios, under any comparison operator satisfying the laws of logic, is equivalent to the arithmetic forced by Booleans. In plain terms: whether you start with a continuous continuum of positive ratios or a two-element Boolean set, the same natural-number arithmetic emerges. This is the first strict cross-realization invariance theorem in the framework. It demonstrates that the natural numbers are not an accident of a particular construction but a forced consequence of the logical structure itself.

The practical consequence is that the framework's foundational arithmetic is independent of the choice of carrier. A reader might worry that building arithmetic from Booleans would give a degenerate or trivial structure. The module shows the opposite: the strict Boolean realization is a faithful and full realization of the same arithmetic that positive ratios force. This means the framework's claims about arithmetic do not depend on a specific model; they hold across radically different carriers, from continuous ratios to discrete truth values.

/-- First strict cross-realization invariance theorem:
positive ratios and Boolean propositions force the same arithmetic. -/
noncomputable def strictPositiveRatio_arith_equiv_strictBoolean
    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
    (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h)).peano.carrier
      ≃ (StrictLogicRealization.arith strictBooleanRealization).peano.carrier :=
  ArithmeticOf.equivOfInitial
    (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h))
    (StrictLogicRealization.arith strictBooleanRealization)

/-- Strict Boolean forced arithmetic is canonically `LogicNat`. -/
def strictBoolean_arith_equiv_logicNat :
    (StrictLogicRealization.arith strictBooleanRealization).peano.carrier
      ≃ ArithmeticFromLogic.LogicNat :=
  (StrictLogicRealization.toLightweight strictBooleanRealization).orbitEquivLogicNat

def boolCost (p q : Bool) : Nat :=
  if p = q then 0 else 1

What this page does not claim

This module does not prove that the Boolean cost function is the unique cost satisfying the framework's axioms. The equivalence does not imply that the Boolean carrier itself is infinite; the carrier orbit remains periodic. The module does not address the physical recognition-to-linking bridge that connects arithmetic to spatial dimensions.

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/UniversalForcing/Strict/DiscreteBoolean.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: