Every integer square is nonnegative

Identifier: F:int-sq-nonneg
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every integer a, 0 <= a * a.

Formal statement

theorem Int.sq_nonneg : ((x0 : Int) -> Int.le Int.zero (Int.mul x0 x0))

Dependencies

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

2 direct dependencies 2 direct dependents

Evidence

kernel-Int.sq_nonneg

Kind: kernel-term
Status: checked

Supports: For every integer a, 0 <= a * a.

Checker command

cargo test -p axeyum-lean-kernel --lib int_prelude

Evidence notes

`build_int_prelude` admits this theorem through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so a green run of the command is a machine-checked proof. Measured 2026-08-15: 12 tests pass -- a NONZERO count, so the filter is not inert. The unconditional form matters and is not `Int.mul_nonneg` specialised: `mul_nonneg` needs both factors nonnegative and says nothing about a negative a.

footprint-Int.sq_nonneg

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- this theorem's trusted closure is empty

Checker command

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

Evidence notes

The third tab-separated column is `Kernel::axiom_footprint` for this declaration, and the regex requires it to be EMPTY -- the rendered type must begin immediately after the name. The discriminating negative control is in the same output: `Int.euclidean_decomposition`, the one integer law still asserted, prints its own name in that column and fails the same regex (measured 2026-08-15). `nat_axiom_inventory` independently reports `nat: axiom=0 opaque=0 quotient=0` for the development ZZ is constructed over, covering all three trusted kinds rather than `Declaration::Axiom` alone.

Provenance

{
  "date": "2026-08-15",
  "established_by": "axeyum-lean-kernel build_int_prelude, lane real-keystone",
  "source": "the one law of the axiomatized `AxReal` package (`AxReal.sq_nonneg`, the nonnegativity primitive each SOS square rests on) that had no `Int` counterpart; proving it completed ZZ as a model of all 30 AxReal axioms (ADR-0456)"
}