Every natural number is below its successor

Identifier: F:nat-le-succ
Proof route: imported-kernel-lean
External status: proved
Axiom footprint: lean4export-3.1.0-stream-faithfulness, axeyum-lean-import-wire-translation, lean4export-3.1.0-delivered-bytes-are-the-intended-export

Recorded description

For every natural number n, n is less than or equal to n + 1.

Formal statement

((n : Nat) -> LE.le.{0} Nat instLENat n (Nat.succ n))

Dependencies

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

0 direct dependencies 4 direct dependents

Evidence

import-Nat.le_succ

Kind: kernel-term
Status: checked

Supports: `Nat.le_succ`'s Lean proof term type-checks against this statement in the independent Axeyum kernel.

Checker command

test "$(cargo test -p axeyum-lean-import --test imported_fact_evidence -- --nocapture 2>/dev/null | grep -c 'AXEYUM-IMPORT-FACT|F:nat-le-succ|')" -ge 1

Evidence notes

The command greps for this fact's own marker line rather than trusting the exit status, so a suite that compiles to zero tests -- this repository's signature defect -- fails instead of exiting 0. Measured 2026-08-15: the stream hashes to the pin in `artifacts/lean-imports/MANIFEST.json`, the fail-closed importer admits 14 declarations (it publishes nothing unless the WHOLE stream translates and every declaration passes the trusted gate), and `Kernel::render_lean` of the admitted type is `((n : AxNat) -> LE.le.{0} AxNat instLENat n (AxNat.succ n))`. `formal.statement` is that string with `render_lean`'s emit-direction `AxNat` guard undone: the renderer rewrites a root `Nat` to `AxNat` so that emitting OUR prelude does not shadow Lean's builtin `Nat`, which is correct in the emit direction and exactly backwards for an import, where the `Nat` in the stream IS Lean's builtin. The test pins both strings.

footprint-Nat.le_succ

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: the imported proof term reaches no Lean axiom, opaque or quotient declaration

Checker command

scripts/check-imported-fact-lean-axioms.sh Nat.le_succ

Evidence notes

Two kernels, independently. `Kernel::axiom_footprint` walks this declaration's transitive dependencies in the IMPORTED environment and reports an empty footprint; a real Lean 4.30.0 binary's `#print axioms Nat.le_succ` reports no axioms. The first three entries are the assumptions the IMPORT adds and the constructed `kernel-lean` route does not make: that the exporter faithfully rendered Lean's environment, that our NDJSON-to-kernel-term translation preserves meaning, and that the delivered bytes are the producer's intended export -- format 3.1 has no footer, so completion is relative to the bytes handed over, which `axeyum-lean-import`'s own documentation states. They are why `axiom_footprint: []` is unavailable on this route and the validator rejects it (ADR-0454).

Provenance

{
  "date": "2026-08-15",
  "established_by": "axeyum-lean-import, lane formalized-collect -- our independent kernel ADMITTED Lean's proof term. This project did NOT construct the proof; see proof_route.",
  "source": "official lean4export NDJSON 3.1.0 stream artifacts/lean-imports/nat-le-succ.ndjson, declaration `Nat.le_succ` from Lean 4.30.0 `Init`",
  "prior_art": [
    {
      "who": "the Lean 4 developers (leanprover/lean4)",
      "what": "`Nat.le_succ` in the Lean 4 core library (`Init`), with its proof term",
      "where": "leanprover/lean4 v4.30.0, githash d024af099ca4bf2c86f649261ebf59565dc8c622",
      "year": 2026,
      "attribution": "read directly from the pinned `lean4export` stream that this fact cites, and cross-checked against a real Lean 4.30.0 binary; this lane did not consult a paper or a secondary source."
    }
  ]
}