landAux fuel-irrelevance: any sufficient fuel agrees with the canonical one

Identifier: F:nat-land-aux-eq-land-of-le
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

For every fuel, m, n with m <= fuel, unfolding Nat.landAux at that fuel gives the same result as Nat.land m n.

Formal statement

theorem Nat.land_aux_eq_land_of_le : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat.le x1 x0) -> Eq.{1} AxNat (AxNat.landAux x0 x1 x2) (AxNat.land x1 x2)))))

Dependencies

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

0 direct dependencies 2 direct dependents

Evidence

kernel-Nat.land_aux_eq_land_of_le

Kind: kernel-term
Status: checked

Supports: for every fuel, m, n with m <= fuel, landAux fuel m n = land m n

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- land_aux_eq_land_of_le 2>/dev/null | grep -Ec '^Nat\.land_aux_eq_land_of_le[[:space:]]')" -ge 1

Evidence notes

`build_nat_prelude` admits this theorem through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so producing this row at all is a machine-checked proof. `nat_theorem_inventory` exits non-zero for a name that does not exist, and `grep -Ec` consumes the pipe and the tested count is what decides the exit status. Anchored with `^Nat\.land_aux_eq_land_of_le[[:space:]]` so a future `_of_le_` sibling cannot satisfy this row.

compute-Nat.land_aux_eq_land_of_le

Kind: kernel-term
Status: checked

Supports: the hypothesis Le m fuel is load-bearing, and the theorem is exactly this, not a weaker or vacuous restatement

Checker command

cargo test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::land_fuel_irrelevance_holds_above_canonical_fuel_with_an_insufficient_fuel_negative_control

Evidence notes

Applies the theorem symbolically (against a free `Le m fuel` hypothesis) and at the concrete instance `(fuel, m, n) = (7, 1, 7)`, where `fuel` STRICTLY EXCEEDS the canonical `m`; both `landAux 7 1 7` and `land 1 7` reduce to `1`. The mandatory negative control checks, BY EVALUATION alone (not through this theorem, since `Le 7 1` has no proof), that at INSUFFICIENT fuel the two sides genuinely disagree: `landAux 1 7 7 = 1` while `land 7 7 = 7` -- the same `(1, 7, 7)` witness the `rec_agreement` lane pinned for `bitwise_aux_eq_land_aux`. Without this the theorem's `Le m fuel` hypothesis could be vacuously true of a stronger, unconditional (and false) statement.

footprint-Nat.land_aux_eq_land_of_le

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Nat prelude's trusted surface is empty

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free nat

Evidence notes

`nat_axiom_inventory --require-axiom-free nat` enumerates the built Nat environment and exits non-zero unless it admits no Axiom, Opaque or Quotient declaration.

Provenance

{
  "date": "2026-08-29",
  "established_by": "axeyum-lean-kernel build_nat_prelude, lane nat-fuel-irrelevance",
  "source": "`declare_land_fuel_irrelevance_all` (`crates/axeyum-lean-kernel/src/nat_prelude/rec_agreement.rs`)"
}