Foundation Discrete Logic Realization Bool Realization

A Boolean ledger

The Boolean realization is a ledger, a discrete record of events, built from the two classical truth values true and false. Its cost function, the price of telling two entries apart, is the simplest possible: zero when the entries match, one when they differ. This is a definitional choice, a model, not a theorem; the framework chooses this carrier to test whether its central forcing argument survives outside the continuous case.

The framework's library, a machine-checked collection of formal theorems, proves that this discrete system obeys the same structural laws as any other realization. The cost is symmetric, meaning the price of comparing true to false equals the price of comparing false to true. The identity step, the act of comparing an entry with itself, costs zero. These are the plain properties one expects from any fair comparison.

The substantive result is invariance. The library proves that the arithmetic forced out of this Boolean ledger is isomorphic to the arithmetic forced out of every other realization, and that this arithmetic has the standard Peano surface, the familiar structure of natural numbers with successor, addition, and multiplication. In plain terms, the framework shows that a system with only two states still generates the same counting arithmetic as any richer system. The discrete case is not a degenerate outlier; it is a faithful carrier of the same forced structure.

What the declaration does not claim is equally sharp. It does not claim that Boolean logic itself is the fundamental substrate of reality, only that it serves as one valid test case for the forcing principle. It does not claim that the two-valued cost function is derived from the five conditions; that uniqueness theorem applies to the continuous J-cost, not to this discrete model. And it does not claim that the isomorphism extends to any physical interpretation; the bridge from these formal realizations to actual physics remains open.

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

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 hqp; exact h hqp.symm
    simp [boolCost, h, h']

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

/-- 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 cost function is not derived from the five forcing conditions; it is a chosen model. The isomorphism does not extend to any physical claim about the structure of space or matter.

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: