A self-map of a finite initial segment is either injective there or has an explicit duplicate pair, constructively

Identifier: F:nat-injective-on-or-duplicate
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every g : Nat -> Nat and every n, either g is injective on [0,n) (Nat.injectiveOn g n) or there exist a < b < n with g a = g b. Constructive: no excluded middle and no classical choice. Built from two nested instances of Nat.lnp_bounded_search, the bounded least-element search for a pointwise-decided predicate. The inner search, at a fixed index i, looks for a j strictly below i with g j = g i, decided pointwise by Nat.beq; searching strictly below i is what makes the produced pair automatically distinct, so the conclusion states Lt a b rather than a negated equality. The outer search runs that decision over [0,n): its no-witness branch yields injectivity through Nat.trichotomy, each strict side building a collision at the larger of the two indices; its witness branch is the duplicate pair.

Formal statement

theorem Nat.injective_on_or_duplicate : ((x0 : ((x0 : AxNat) -> AxNat)) -> ((x1 : AxNat) -> Or (AxNat.injectiveOn x0 x1) (Exists.{1} AxNat (fun (x2 : AxNat) => Exists.{1} AxNat (fun (x3 : AxNat) => And (AxNat.lt x2 x1) (And (AxNat.lt x3 x1) (And (AxNat.lt x2 x3) (Eq.{1} AxNat (x0 x2) (x0 x3)))))))))

Dependencies

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

7 direct dependencies 1 direct dependents

Evidence

kernel-Nat.injective_on_or_duplicate

Kind: kernel-term
Status: checked

Supports: `Nat.injective_on_or_duplicate` is in the environment as a checked `Declaration::Theorem` with an EMPTY `Kernel::axiom_footprint`. The `formal.statement` above is `Kernel::render_lean` of the admitted type, printed by `nat_theorem_inventory` (the `3` in the row is the free-variable count; the footprint is checked by the second row).

Checker command

scripts/cargo-serialized.sh run --release -p axeyum-lean-kernel --example nat_theorem_inventory -- injective_on_or_duplicate 2>/dev/null | /usr/bin/grep -cE 'Nat\.injective_on_or_duplicate[[:space:]]3[[:space:]]'

Evidence notes

Run 2026-09-02: one row, count 1. `nat_theorem_inventory` consumes only its LAST name argument, so this command passes exactly one name; a filter matching nothing prints no row and `grep -c` then exits 1.

suite-Nat.injective_on_or_duplicate

Kind: kernel-term
Status: checked

Supports: `nat_prelude_tests::every_nat_declaration_is_checked_and_axiom_free` derives its population from `kernel.environment()` rather than from a literal list, so it fails both if this declaration rests on an axiom and if it were dropped from the checked list while remaining in the environment.

Checker command

test "$(scripts/cargo-serialized.sh test --release -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::every_nat_declaration_is_checked_and_axiom_free -- --exact 2>&1 | /usr/bin/grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

Run 2026-09-02: `test result: ok. 1 passed; 0 failed`.

Provenance

{
  "date": "2026-09-02",
  "established_by": "axeyum-lean-kernel build_nat_prelude (crates/axeyum-lean-kernel/src/nat_prelude/injective_decide.rs)",
  "source": "Lane det-mul-general-n, closing ADR-1440's obligation 2 (the selection lemma) on the way to determinant multiplicativity at symbolic n. Status note: docs/plan/status/det-mul-general-n.md."
}