Int.even_iff_nat_abs_even : forall n, Iff (Odd n) (Nat.Odd (natAbs n))

Identifier: F:int-even-iff-nat-abs-even
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

For every n : Int, Int.Even n holds iff Nat.Even (Int.natAbs n) holds. Named, discoverable API surface for what Int.Odd's own definition (F:int-even) already gives for free: both directions of the Iff are the identity function, since the two sides are the SAME term up to one delta unfold of Int.Odd.

Formal statement

theorem Int.even_iff_nat_abs_even : ((x0 : Int) -> Iff (Int.Even x0) (AxNat.Even (Int.natAbs x0)))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-Int.even_iff_nat_abs_even

Kind: kernel-term
Status: checked

Supports: Int.even_iff_nat_abs_even is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example int_theorem_inventory 2>/dev/null | grep -cE '^theorem[[:space:]]Int\.even_iff_nat_abs_even[[:space:]]'

Evidence notes

int_theorem_inventory lists every Declaration::Theorem in the integer prelude with its canonical type; the grep asserts the exact tab-anchored name. --release is MANDATORY: this binary also builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-Int.even_iff_nat_abs_even

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude's trusted surface is empty, which bounds Int.even_iff_nat_abs_even

Checker command

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

Evidence notes

Re-measured on this tree: integer trusted surface = 0. --release is MANDATORY here.

coverage-Int.even_iff_nat_abs_even

Kind: witness-replay
Status: checked

Supports: int_prelude_tests.rs's every_int_declaration_is_checked_and_axiom_free asserts, against the ENVIRONMENT rather than a hand-maintained list, that every live Int.* Definition/Theorem (this one included) is listed in derived_laws/derived_lemmas/asserted_laws/definition_names and carries an empty axiom footprint.

Checker command

cargo test -p axeyum-lean-kernel --lib int_prelude::int_prelude_tests::every_int_declaration_is_checked_and_axiom_free 2>&1 | grep -c '^test result: ok\. 1 passed'

Evidence notes

Guards against the class of gap CLAUDE.md documents repeatedly: a Definition/Theorem live in the prelude but absent from every hand-maintained list, which would otherwise receive no axiom-footprint check at all.

Provenance

{
  "date": "2026-08-28",
  "established_by": "axeyum-lean-kernel build_int_prelude (crates/axeyum-lean-kernel/src/int_prelude/parity.rs, declare_even_iff_nat_abs_even)",
  "source": "canonical type read via int_theorem_inventory's own output (cargo run -q --release -p axeyum-lean-kernel --example int_theorem_inventory), which prints one row per Declaration::Theorem in the integer prelude with kernel.render_lean(declaration.ty()) as the last field. That row was grepped and copied verbatim into formal.statement. No new probe binary was written; crates/ source was touched only to add the declaration itself and its test."
}