Foundation Universal Forcing Strict Discrete Boolean Xor Bool

The Boolean realization

In ordinary computing, xor is the exclusive-or gate: it outputs true when its two inputs differ, and false when they match. The Recognition Science framework defines a Boolean realization of its core logic using exactly this operation, written xorBool. The definition is minimal: xorBool p q is simply xor p q, the standard Boolean exclusive-or. This is a definitional choice, a model, not a theorem about the physical world.

The framework's ledger, a discrete record of recognition events, can be realized in many carriers. The Boolean realization is one such carrier, using only two values, true and false. The framework pairs xorBool with a cost function, boolCost, which assigns 0 when two Boolean values are equal and 1 when they differ. Two properties of this cost are proved in the machine-checked library of formal theorems: boolCost_self establishes that the cost of comparing a value to itself is always 0, and boolCost_symm establishes that the cost is symmetric, meaning the order of comparison does not matter.

The significant result is what this two-valued carrier forces. The framework proves that the arithmetic derived from the Boolean realization is canonically equivalent to LogicNat, the framework's natural-number arithmetic. More strongly, a theorem shows that positive ratios and Boolean propositions force the same arithmetic: strictPositiveRatio_arith_equiv_strictBoolean establishes an equivalence between the arithmetic forced by positive ratios and the arithmetic forced by the Boolean realization. In plain terms, whether the ledger starts from continuous ratios or from a two-valued logic gate, the same counting arithmetic emerges.

What xorBool does not claim is broader than what it establishes. It does not claim that the physical world is Boolean at its base, nor that xor is the fundamental operation of the universe. It establishes a structural fact: a two-valued realization of the framework's logic yields the same arithmetic as a continuous one. The carrier is periodic, as the source notes, but the strict forced arithmetic is the free iteration object derived from the native generator, not the finite image inside Bool. This is a result about the framework's internal consistency across realizations, not a claim about the ultimate nature of computation or physics.

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

/-- 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)

@[simp] theorem boolCost_self (p : Bool) : boolCost p p = 0 := by
  simp [boolCost]

theorem boolCost_symm (p q : Bool) : boolCost p q = boolCost q p := by
  by_cases h : p = q
  · subst h
    simp [boolCost]
  · have h' : q ≠ p := by intro hq; exact h hq.symm
    simp [boolCost, h, h']

What this page does not claim

xorBool does not claim that physical reality is Boolean at its base. The equivalence does not claim that the Boolean carrier is not periodic in its strict arithmetic. The framework does not claim that xor is the fundamental operation of the universe.

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: