Delta Kernel Examples One Plus One Forced

The forced sum

The declaration onePlusOne_forced in the framework's machine-checked library of formal theorems establishes that the statement 1 + 1 = 2 is derivable from the fundamental recursion equations that define addition, without invoking induction, without assuming any logical posits, and without appealing to any external axioms. The proof is a concrete derivation tree, a step-by-step construction that the kernel itself verifies by direct computation. The tree uses the equation 1 + 0 = 1 and the rule that 1 + S0 = S(1 + 0), where S is the successor function, to rewrite the expression and conclude that 1 + 1 equals 2. The kernel's check returns a result tagged as forced, meaning the derivation is accepted and the ledger, the framework's discrete record of which logical assumptions were used, is empty.

This is a worked example in a larger project that tests how much of mathematics can be forced from minimal starting points. The same file contains a companion proof that 0 + n = n for every natural number n, which does use induction, and a demonstration that the law of excluded middle, the principle that every statement is either true or false, is not needed for this particular concrete instance of 0 = 0. The onePlusOne_forced proof is the simplest case: it shows that even the most basic arithmetic fact can be certified as a forced consequence of the recursion equations alone. A separate host theorem, one_plus_one_certified, exports this result to the standard natural number type, confirming that 1 + 1 = 2 holds in the ordinary sense.

What the declaration does not claim is just as important. It does not claim that all of arithmetic can be derived without induction; the zeroAdd example explicitly requires induction, and the kernel distinguishes between quantifier-free induction and full induction on quantified formulas. It does not claim that the law of excluded middle is never needed; the file shows the same disjunction 0 = 0 or not(0 = 0) can be obtained both with and without the excluded-middle posit, and the ledger records the difference. It does not claim that the framework's approach replaces or contradicts standard mathematics; the certified theorem 1 + 1 = 2 is the same fact any arithmetic system proves. The declaration is a proof of one specific equation under one specific set of rules, not a claim about the foundations of all mathematics.

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

What this page does not claim

Not a claim that all arithmetic can be derived without induction. Not a claim that the law of excluded middle is never needed in the framework. Not a claim that this proof replaces or contradicts standard mathematics.

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: