No integer lies strictly between zero and one

Identifier: F:int-no-integer-strictly-between-zero-and-one
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

There is no integer x with 0 < x and x < 1.

Formal statement

theorem Int.no_int_between : ((x0 : Int) -> Not (And (Int.lt Int.zero x0) (Int.lt x0 Int.one)))

Dependencies

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

4 direct dependencies 2 direct dependents

Evidence

kernel-Int.no_int_between

Kind: kernel-term
Status: checked

Supports: There is no integer x with 0 < x and x < 1.

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-14: 12 tests pass (a nonzero count -- the filter is not inert).

footprint-Int.no_int_between

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 -- no_int_between 2>/dev/null | grep -Ec '^theorem[[:space:]]+Int\.no_int_between[[:space:]]')" -ge 1

Evidence notes

Two independent bounds, because either alone would be weaker than it looks. (1) `Kernel::axiom_footprint` walks THIS declaration's transitive dependencies and prints an empty footprint column -- this is the kernel's `#print axioms`, and it is the check that matters, since an integer law IS still asserted (`Int.euclidean_decomposition`; it was 6 until lane int-remainder proved the `subNatNat` borrow, and the check mattered more then) and Int.no_int_between could have reached for one and still type-checked. (2) `nat_axiom_inventory` reports `nat: axiom=0 opaque=0 quotient=0` for the development ZZ is constructed over, so the foundation admits no trusted declaration at all. Counting `Declaration::Axiom` alone would not have sufficed: `Opaque` has no proof body and `Quotient` admits `Quot.sound`, which is exactly the declaration the quotient-of-NxN construction would have added -- the enumeration covers all three kinds and reports zero for each.

applied-Int.no_int_between

Kind: kernel-term
Status: checked

Supports: the theorem is usable as a refutation, not merely well-typed

Checker command

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

Evidence notes

Applies the theorem to an abstract `x : Int` and a conjunction built from hypotheses `0 < x` and `x < 1`, then `infer`s the result and checks it is definitionally `False`. This is the step the Diophantine refutation route actually performs.

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum-lean-kernel build_int_prelude, lane int-keystone",
  "source": "one of the 34 propositions build_int_prelude previously ASSERTED; this lane constructed ZZ over the proved Nat development and derived it"
}