Eisenstein's floor-sum identity without the min

Identifier: F:nat-eisenstein-floor-sum-min-free
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For coprime odd `pp = 2m+1` and `q = 2n+1`: `SUM_{x<m} floor(q(x+1)/pp) + SUM_{y<n} floor(pp(y+1)/q) = n*m`, with NO `Min.min` anywhere. This is ADR-1544's residue 5. WHY THE MIN IS THERE IN THE GENERAL THEOREM AND CAN COME OFF HERE: ADR-1290's floor lemma produces `Min.min n floor(.)` because a rectangle's row count is capped by its height, and ADR-1544 MEASURED that dropping the min from `Nat.eisenstein_floor_sum` is REFUTED at the generality that theorem states and SURVIVES only at Eisenstein's own `m = (p-1)/2`, `n = (q-1)/2`. This turns that recorded survivor into a theorem: at `pp = 2m+1`, `q = 2n+1` the cap never binds, by `Nat.div_mul_succ_le_of_le`, so `Nat.min_eq_right` removes it under two `Nat.sumRange_congr_lt`s, one per axis. THE RESTRICTION IS LOAD-BEARING AND IS REFUTED INSIDE THE KERNEL: at `pp = 2`, `q = 5`, `m = 1`, `n = 0` -- a general instance `Nat.eisenstein_floor_sum` also reaches, since `gcd 2 5 = 1` and `1 < 2` -- the cap DOES bind, the bare row sum reduces to `2`, the capped one to `0`, and `def_eq` rejects the two. That reproduces ADR-1544's `M4`. `Kernel::axiom_footprint` is EMPTY. Admitted on the first attempt.

Formal statement

theorem Nat.eisenstein_floor_sum_min_free : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : Eq.{1} AxNat (AxNat.gcd (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0)) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x1))) (AxNat.succ AxNat.zero)) -> Eq.{1} AxNat (AxNat.add (AxNat.sumRange (fun (x3 : AxNat) => AxNat.div (AxNat.mul (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x1)) (AxNat.succ x3)) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) x0) (AxNat.sumRange (fun (x3 : AxNat) => AxNat.div (AxNat.mul (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0)) (AxNat.succ x3)) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x1))) x1)) (AxNat.mul x1 x0))))

Dependencies

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

7 direct dependencies 1 direct dependents

Evidence

kernel-Nat.eisenstein_floor_sum_min_free

Kind: kernel-term
Status: checked

Supports: Nat.eisenstein_floor_sum_min_free 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 theorem_dependency_inventory -- Nat.eisenstein_floor_sum_min_free 2>/dev/null | grep -cE '^Nat\.eisenstein_floor_sum_min_free[[:space:]]'

Evidence notes

Two independent failure modes, so the exit status depends on the finding rather than on the run completing: theorem_dependency_inventory exits non-zero when a NAMED filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. RUN WITH A NEGATIVE CONTROL and it was: the real name prints 1 with both pipeline stages at 0, a one-character typo prints 0 with both stages at 1. Anchored with [[:space:]], never \t -- in a scripted (GNU) grep \t is a literal t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY, and so is a FRESH build: this lane hit the stale-binary trap here, and a prebuilt inventory reported this very theorem ABSENT. `cargo run` rebuilds; a prebuilt binary does not. Pass ONE name per invocation.

footprint-Nat.eisenstein_floor_sum_min_free

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the natural-number prelude's trusted surface is empty, which bounds Nat.eisenstein_floor_sum_min_free.

Checker command

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

Evidence notes

--require-axiom-free exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is not empty, and errors rather than silently passing for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty nat surface bounds every declaration in it. This is a whole-prelude bound, not a per-declaration measurement; the per-declaration figure is measured 0 by the axiom-footprint assertion in eisenstein_floor_min_free_tests.rs.

numeric-Nat.eisenstein_floor_sum_min_free

Kind: exhaustive-enumeration
Status: checked

Supports: C6 of ADR-1552's check script verifies the min-free identity at 317 coprime odd pairs, and C6b verifies separately that the cap never binds on either axis at any of them -- the fact the bound lemma states. M11 refutes the same reading at pp=2, q=5, m=1, n=0, a general instance where the cap does bind.

Checker command

python3 docs/research/09-decisions/adr-1552-eisenstein-checks.py

Evidence notes

Exit status depends on the finding: a claim that fails, or a control that behaves other than as recorded, exits 1. Verified by mutating the script itself in a scratch copy with one uniquely-named file per mutant: 19 of 19 mutations exit 1, including shifting the min-free floor sum, making C6b's cap check fire spuriously, and making M11's witness satisfy the cap. TWO mutations were deliberately NOT run and the omissions are recorded: vacuity edits (`if FAILURES:` and C6b's cap condition replaced by `if False:`) are no-ops against a PASSING baseline, so running them would measure nothing.

Provenance

{
  "date": "2026-09-02",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_nat_prelude (crates/axeyum-lean-kernel/src/nat_prelude/eisenstein_floor_min_free.rs)",
  "source": "formal.statement is taken verbatim from the kernel's own rendering (Kernel::render_lean of the admitted declaration type; the same string is pinned character for character in eisenstein_floor_min_free_tests.rs). depends_on is the direct-theorem column of theorem_dependency_inventory intersected with this ledger's registered facts, so it is an INTERSECTION and not the full dependency set. Nothing about the statement was hand transcribed; title, statement and the evidence notes were authored (lane eisenstein-3)."
}