Euclidean decomposition over the integers is derived, not assumed

Identifier: F:int-euclidean-decomposition
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For all integers t and k with 0 < k, there exist integers q and r such that t = k*q + r and 0 <= r < k. Established here as a THEOREM: the integer prelude, which previously asserted this, now assumes nothing at all.

Formal statement

theorem Int.euclidean_decomposition : ((x0 : Int) -> ((x1 : Int) -> ((x2 : Int.lt Int.zero x1) -> Exists.{1} Int (fun (x3 : Int) => Exists.{1} Int (fun (x4 : Int) => And (Eq.{1} Int x0 (Int.add (Int.mul x1 x3) x4)) (And (Int.le Int.zero x4) (Int.lt x4 x1)))))))

Dependencies

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

6 direct dependencies 1 direct dependents

Evidence

kernel-Int.euclidean_decomposition

Kind: kernel-term
Status: checked

Supports: For all integers t and k with 0 < k, there exist q and r with t = k*q + r and 0 <= r < k.

Checker command

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

Evidence notes

The `^theorem` anchor is the whole point of this row, not decoration. Until 2026-08-16 this declaration was an `axiom`, and the same command would print an `axiom` row and FAIL the grep. So the checker discriminates exactly the change the fact records -- it is bound to this declaration's name AND to its kind, and `int_theorem_inventory` additionally exits non-zero for a name that does not exist.

footprint-integer

Kind: exhaustive-enumeration
Status: checked

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

Checker command

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

Evidence notes

Enumerates the built Int environment over the FULL trusted surface (Axiom/Opaque/Quotient) and exits non-zero on any member. Environment-wide on purpose, and sound as a footprint bound for the same reason the Nat rows are: a theorem cannot depend on a trusted declaration the environment does not contain, so an empty surface bounds every individual footprint by []. Measured 2026-08-16: `ok: integer trusted surface = 0`, down from 34 when the construction began.

Provenance

{
  "date": "2026-08-16",
  "established_by": "axeyum-lean-kernel int_prelude (int-euclid lane)",
  "source": "hand-built foundational library"
}