Mathlib v4.30 source proposition Nat.even_div

Identifier: F:ml430-nat-even-div-395c6b5e
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The proposition declared as `Nat.even_div` in the pinned Mathlib v4.30 source.

Formal statement

∀ {m n : ℕ}, Even (m / n) ↔ m % (2 * n) / n = 0

Dependencies

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

3 direct dependencies 0 direct dependents

Evidence

kernel-Nat.even_div

Kind: kernel-term
Status: checked

Supports: `Nat.even_div` is admitted as a Theorem with EXACTLY the mirror's shape, pinned verbatim via the kernel's own renderer. Reduces to `Nat.even_iff_mod_two_eq_zero` at `q := m/n`, bridged through `Nat.mod_mul_right_div_self` (an UNCONDITIONAL digit-decomposition identity already in `mod_mul_lemmas.rs`: `m % (n*k) / n = (m/n) % k`, at `k := 2`) and `Nat.mul_comm` (to align `2*n`/`n*2`), transported along the resulting `Eq` via `Eq.rec` directly. No new arithmetic lemma.

Checker command

test "$(cargo run -q --release -p axeyum-lean-kernel --example nat_theorem_inventory even_div 2>/dev/null | awk -F'\t' '$1 == "Nat.even_div" && $3 == "((x0 : AxNat) -> ((x1 : AxNat) -> Iff (AxNat.Even (AxNat.div x0 x1)) (Eq.{1} AxNat (AxNat.div (AxNat.mod x0 (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x1)) x1) AxNat.zero)))"' | wc -l)" -ge 1

instance-Nat.even_div

Kind: kernel-term
Status: checked

Supports: Applies at a concrete `(m, n) := (7, 3)` (`q := 2` Even, `7 % 6 / 3 = 0`) with REAL witnesses on both `mp` (a genuine `Even 2`) and `mpr` (`Eq 0 0` by `refl`) legs, each confirmed by `def_eq` against the computed reduct; plus a truncation control at `(9, 3)` (`q := 3` Odd) confirming `9 % 6 / 3` genuinely computes to `1`, not `0` -- the residue a wrong scaling/truncation formula would miss; plus genuinely free `m`, `n`.

Checker command

test "$(cargo test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::even_div_applies_at_concrete_pairs_and_rejects_a_wrong_residue_control -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

footprint-Nat.even_div

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for `Nat.even_div`. The `nat` prelude's trusted surface stays 0: no Axiom, no Opaque, no Quotient.

Checker command

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

coverage-Nat.even_div

Kind: kernel-term
Status: checked

Supports: Coverage for `Nat.even_div` derived from `kernel.environment()` directly, not from an inventory list -- a Nat-namespace declaration missing from `theorem_names` fails this test by name.

Checker command

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

Provenance

{
  "date": "2026-08-29",
  "established_by": "lane parity-finish (2026-08-30): built directly as a kernel declaration in the new file nat_prelude/even_div.rs. The prior lane (nat-parity-div) had sized this as needing a new div/mod-scaling identity built from `div_mod_exec`/`div_mod_unique`; instead it reduces to `Nat.even_iff_mod_two_eq_zero` at `q := m/n` via the ALREADY-EXISTING unconditional `Nat.mod_mul_right_div_self` (`mod_mul_lemmas.rs`) at `k := 2`, bridged by `Nat.mul_comm` and `Eq.rec` transport -- no new arithmetic lemma. Verified against the pinned Mathlib v4.30.0 source (commit c5ea00351c28e24afc9f0f84379aa41082b1188f) that this is a standard Nat division/parity lemma about the SAME `Nat.div`/`Nat.mod`/`Nat.Even` this kernel already has (no new definition introduced), so mirroring it under Mathlib's own name is honest under the mirror-flip criterion.",
  "source": "statement-only extraction of `Nat.even_div` from Mathlib v4.30.0; no proof value was exposed",
  "prior_art": [
    {
      "who": "the Mathlib contributors",
      "what": "the theorem declaration `Nat.even_div`",
      "where": "mathlib4 commit c5ea00351c28e24afc9f0f84379aa41082b1188f (v4.30.0)",
      "year": 2026,
      "attribution": "the proposition was read from the pinned statement-only inventory; the proof term and tactic trace were not consulted"
    }
  ]
}