Q proves every true numeral addition and every true numeral multiplication

Identifier: F:fo-q-numeral-arithmetic
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For all naturals a and b, the seven Robinson axioms prove the object-level equation between the sum of the numerals for a and b and the numeral for a + b, and likewise for the product and a * b. The numerals are FO.Term.numeral -- the same function the Goedel numbering of fo_roundtrip.rs codes -- and both statements quantify over a and b symbolically rather than over literals.

Formal statement

theorem FO.Q.add_numeral : ((x0 : AxNat) -> ((x1 : AxNat) -> FO.Provable FO.Q (FO.Formula.eqf (FO.Term.f2 AxNat.zero (FO.Term.numeral x0) (FO.Term.numeral x1)) (FO.Term.numeral (AxNat.add x0 x1)))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

1 direct dependencies 1 direct dependents

Evidence

kernel-FO.Q.add_numeral

Kind: kernel-term
Status: checked

Supports: FO.Q.add_numeral is admitted by the trusted kernel gate with the type recorded in formal.statement, and rests on no axiom. Nat.rec on the SECOND argument, mirroring the recursion in Nat.add and in the axiom axAddSucc, so the successor step is ONE application of the Leibniz rule FO.Provable.eqf_subst against the induction hypothesis, with no separate object-level congruence or transitivity lemma.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_robinson_inventory -- FO.Q.add_numeral --exact --require-axiom-free

Evidence notes

Declared in crates/axeyum-lean-kernel/src/fo_robinson.rs by declare_add_numeral.

kernel-FO.Q.mul_numeral

Kind: kernel-term
Status: checked

Supports: theorem FO.Q.mul_numeral : ((x0 : AxNat) -> ((x1 : AxNat) -> FO.Provable FO.Q (FO.Formula.eqf (FO.Term.f2 (AxNat.succ AxNat.zero) (FO.Term.numeral x0) (FO.Term.numeral x1)) (FO.Term.numeral (AxNat.mul x0 x1))))) -- admitted by the trusted gate, axiom-free. It DEPENDS on add_numeral, and the test reads that edge out of the kernel's own proof term rather than from the source: axMulSucc gives a * S k = a * k + a, and rewriting a * k to its numeral leaves an object-level SUM rather than a numeral, so add_numeral is what closes it. The control is that the edge does not go the other way.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_robinson_inventory -- FO.Q.mul_numeral --exact --require-axiom-free

Evidence notes

fo_robinson::tests::mul_numeral_depends_on_add_numeral.

the-statements-and-the-instances

Kind: kernel-term
Status: checked

Supports: Both types are pinned against REBUILT expected types rather than against renderings, with a negative control that swapping the two arguments on the right of the equation is a DIFFERENT statement -- Nat.add a b and Nat.add b a are propositionally but not definitionally equal here, because Nat.add recurses on its right argument. Both theorems are then INSTANTIATED at (0,0), (2,3) and (3,1), where the conclusion is checked by def_eq against the arithmetic fact at literal numerals, each row carrying a wrong-numeral negative control.

Checker command

cargo test -p axeyum-lean-kernel --release --lib -- fo_robinson::tests --test-threads=4

Evidence notes

A theorem that could not be applied to a literal would still admit; the instantiation rows are the check that it can be.

footprint-whole-package

Kind: instance-pin
Status: checked

Supports: axiom_footprint: [] -- for all 132 declarations build_fo_robinson_prelude adds on top of the Nat prelude, not only the headline theorem. The row set is a SET DIFFERENCE against a kernel carrying only build_nat_prelude, recomputed on every run, so it is derived from the environment rather than from a hand-maintained list. This package is the first that holds BOTH fo_* chains -- the arithmetization (FO.Code.diagAux_code) and the calculus (FO.soundness) -- in one kernel, so the sweep covers both.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example fo_robinson_inventory -- --require-axiom-free --expect-count 132

Evidence notes

--expect-count fails on drift in EITHER direction, so a declaration silently disappearing is a failure too. The same set difference is recomputed inside the test suite by fo_robinson::tests::the_whole_robinson_package_is_axiom_free, with coverage controls drawn from BOTH chains (FO.Code.diagAux_code and FO.soundness) so it cannot pass vacuously and cannot pass if the two chains stopped composing.

Provenance

{
  "date": "2026-09-06",
  "established_by": "axeyum-lean-kernel build_fo_robinson_prelude, lane fo-representability (W3-7, ADR-1651)",
  "source": "authored from the roadmap item; the axiom list is Robinson's, the encoding, the structure and every proof term are written here",
  "prior_art": [
    {
      "who": "Raphael M. Robinson",
      "what": "the finitely axiomatised essentially undecidable arithmetic Q",
      "year": 1950,
      "where": "R. M. Robinson, 'An essentially undecidable axiom system', Proc. ICM 1950, vol. 1, 729-730",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}