Delta Kernel Examples Full Ind Demo Tier

A proof that uses full induction

Mathematical induction is a standard method for proving a statement about all natural numbers. The simple version, quantifier-free induction, proves a statement about a specific number or a simple pattern. The full version, sometimes called complete or full induction, allows the proof to assume the statement holds for all smaller numbers in order to prove it for the next one. This is a more powerful tool, and it is the one used in many ordinary mathematical arguments.

The declaration fullIndDemo_tier in the framework's machine-checked library of formal theorems demonstrates this distinction concretely. It checks a specific derivation tree, a formal record of each proof step, that uses full induction on a quantified formula. The formula in question states that every number is equal to itself. The checker, which is a program that verifies each step against the kernel's rules, accepts the tree and posts a flag that records the proof's tier as FORCED @ FULL-IND. This is in contrast to another example, zeroAdd, which uses only the weaker quantifier-free induction and is tagged FORCED @ QF-IND.

What this establishes is not a new mathematical fact. The statement that every number equals itself is trivially true. The point is the mechanism: the framework's kernel, not the host's proof search, accepts this particular derivation tree and correctly labels the strength of the induction used. The declaration is a worked example, a concrete test case showing that the checker can handle full induction and that it records the distinction in the proof's tier flag. It is part of a series of examples that demonstrate each verdict class end to end, from the derivation tree to the kernel audit.

In Recognition Science, this is part of the ledger, a discrete record of recognition events. Here the ledger records the cost of a proof: which postulates, such as the law of excluded middle or Markov's principle, were needed to complete it. For fullIndDemo_tier, the ledger shows that the proof required the full induction rule but no other schematic postulates. The declaration does not claim that full induction is the only way to prove this formula, nor does it claim that the framework derives any new arithmetic. It simply demonstrates that the checker accepts this specific proof and that the tier flag is posted correctly.

/-- The kernel accepts `fullIndDemo` and posts the TIER flag: ledger
`ofIndFull` = no posits, full-induction tier. FORCED @ FULL-IND. -/
theorem fullIndDemo_tier :
    check [] fullIndDemo = some (.all quantFormula, .ofIndFull) := by
  decide

/-- The kernel accepts `zeroAdd` with the EMPTY ledger: no posits, and the
QF tier (the induction formula is quantifier-free, so `indFull` stays
`false`). FORCED @ QF-IND. -/
theorem zeroAdd_forced :
    check [] zeroAdd = some (.all zeroAddFormula, .empty) := by
  decide

What this page does not claim

The declaration does not prove any new arithmetic fact, since the formula it checks is trivially true. It does not claim that full induction is necessary for this particular formula, only that this derivation uses it. It does not claim that the framework's checker replaces the host's proof search in general.

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: