Delta Kernel Examples One Plus One Certified

What the certification shows

The statement 1 + 1 = 2 is one of the oldest facts in mathematics. In the Recognition Science framework, the declaration one_plus_one_certified establishes that this equation can be derived by a concrete, machine-checked proof tree that uses no induction and no logical posits. The proof works directly from the recursion equations that define addition: 1 + 0 = 1 and 1 + S0 = S(1 + 0). The framework's kernel, a small executable checker, verifies each step of this derivation. The result is a theorem about natural numbers whose axiom closure is empty, meaning the proof depends on no unstated assumptions. This is the simplest worked example in the framework's library, which is a machine-checked collection of formal theorems.

The declaration is part of a larger demonstration that the framework can produce certified arithmetic. Alongside it, the library contains zero_add_certified, which proves 0 + n = n for every natural number n using induction, and then exports that proof to a host theorem about natural numbers. The kernel audits the derivation tree and records the tier of induction used, distinguishing quantifier-free induction from full induction on quantified formulas. The framework also shows a contrast: the decidable disjunction 0 = 0 or not (0 = 0) can be obtained either by posting the law of excluded middle as a posit, or by a direct introduction rule that leaves the ledger empty. The ledger, a discrete record of which logical posits a proof used, measures the difference. The Markov posit, which accepts only quantifier-free matrices, is shown to reject a quantified formula, with the guard enforced by the checker itself.

In Recognition Science, this worked example serves as the entry point to the framework's core claim: that mathematical structure can be forced by the cost of recognition, and that proofs can be audited to show exactly what they require. The one_plus_one_certified declaration does not prove the general theory of arithmetic, does not establish the forcing chain that leads to constants like the golden ratio, and does not show that all of mathematics can be reduced to this kernel. It is a concrete, verified instance: a single equation, derived from definitions, with a record showing that no schematic logical posit was needed. What it changes for a reader is the picture of what a proof can be: not just a convincing argument, but a tree of steps that a machine can check line by line, with the assumptions made visible.

/-- Exported to the host: `1 + 1 = 2` in `Nat`, certified through the
δ-kernel and the canonical model rather than by host arithmetic. -/
theorem one_plus_one_certified : 1 + 1 = 2 :=
  sound_forced onePlusOne_forced (fun _ => 0)

/-- The kernel accepts `onePlusOne` with the EMPTY ledger: σ0 / DELTA_FORCED. -/
theorem onePlusOne_forced :
    check [] onePlusOne = some (.eq (.add one one) two, .empty) := by
  decide

/-- The kernel accepts `onePlusOne` with the EMPTY ledger: σ0 / DELTA_FORCED. -/
theorem onePlusOne_forced :
    check [] onePlusOne = some (.eq (.add one one) two, .empty) := by
  decide

/-- Exported to the host: `1 + 1 = 2` in `Nat`, certified through the
δ-kernel and the canonical model rather than by host arithmetic. -/
theorem one_plus_one_certified : 1 + 1 = 2 :=
  sound_forced onePlusOne_forced (fun _ => 0)

/-- Route A posts `em`: the verdict is CONDITIONAL {EM}. -/
theorem emRoute_posts_em :
    check [] emRoute = some (.disj zeroEq zeroEq.neg, .ofEM) := by
  decide

/-- Route B proves the SAME formula with the EMPTY ledger: FORCED. -/
theorem forcedRoute_forced :
    check [] forcedRoute = some (.disj zeroEq zeroEq.neg, .empty) := by
  decide

/-- Markov on a quantified matrix: REJECTED by the kernel (not merely
discouraged). -/
theorem mp_rejects_quantified :
    check [] (.mpPosit (.all (.eq (.var 0) (.var 0)))) = none := by
  decide

What this page does not claim

This declaration does not prove the general theory of arithmetic or all of mathematics. It does not establish the forcing chain that leads to constants like the golden ratio. It does not show that the law of excluded middle is never needed in the framework, only that it was not needed for this instance.

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/DeltaKernel/Examples.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: