n mod 2 = 0 or n mod 2 = 1

Identifier: F:nat-mod-two-eq-zero-or-one
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Every natural number's remainder on division by two is either zero or one.

Formal statement

theorem Nat.mod_two_eq_zero_or_one : ((x0 : AxNat) -> Or (Eq.{1} AxNat (AxNat.mod x0 (AxNat.succ (AxNat.succ AxNat.zero))) AxNat.zero) (Eq.{1} AxNat (AxNat.mod x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ AxNat.zero)))

Dependencies

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

3 direct dependencies 7 direct dependents

Evidence

kernel-Nat.mod_two_eq_zero_or_one

Kind: kernel-term
Status: checked

Supports: for every n, n mod 2 = 0 or n mod 2 = 1

Checker command

test "$(cargo run -q -p axeyum-lean-kernel --example nat_theorem_inventory -- mod_two_eq_zero_or_one 2>/dev/null | grep -Ec '^Nat\.mod_two_eq_zero_or_one[[: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. Derived from `Nat.mod_lt` (giving `Lt (mod n 2) 2` from `zero_lt_succ 1`) and `Nat.lt_two_cases`, which is `ops::cases_lt_bound` at `bound = 2` -- no new primitive. `nat_theorem_inventory` exits non-zero for a name that does not exist, and `grep -Ec` consumes the pipe and the count is tested, so the exit status depends on what the run found. Anchored with `^Nat\.mod_two_eq_zero_or_one[[:space:]]` (verified exactly 1 row; the anchor also excludes `Nat.lt_two_cases`, which is a different declaration).

compute-Nat.mod_two_eq_zero_or_one

Kind: kernel-term
Status: checked

Supports: the disjunction is the stated one, its two sides are different propositions, and lt_two_cases applies

Checker command

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

Evidence notes

Applies the theorem at `n = 7` and confirms its INFERRED type is exactly `Or (Eq (mod 7 2) 0) (Eq (mod 7 2) 1)`, with a negative control that it does not also state `Or (Eq (mod 7 2) 0) (Eq (mod 7 2) 2)` -- a control that differs in ONE literal, deliberately, since a control transposing whole subterms would make the kernel run a failing defeq with no early exit. Also asserts the two disjuncts are NOT def_eq to each other, so the split is not vacuous. `Nat.lt_two_cases` is checked in the same test at `r = 0` against a `zero_lt_succ 1` witness.

footprint-Nat.mod_two_eq_zero_or_one

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-rec-agreement",
  "source": "`declare_rec_agreement_all` (`crates/axeyum-lean-kernel/src/nat_prelude/rec_agreement.rs`)"
}