The floor-counting lemma in executable form

Identifier: F:nat-countrange-mul-succ-le-eq-floor
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

`countRange (fun j => ble (mul (succ ap) (succ j)) B) n = Min.min n (div B (succ ap))` -- the same count as `F:nat-countrange-mul-succ-le-eq-min`, with the quotient now named by the executable `Nat.div`. WHY IT IS THE POINT: it is the one place in the family where a division is written down, and it is a single instantiation rather than anything the proof reasons about. HOW IT IS PROVED: `Nat.div_mod_exec ap B : divMod (succ ap) B (div B (succ ap)) (mod B (succ ap))` supplies the relational witness, and `Nat.countRange_mul_succ_le_eq_min` is applied to it. Positivity of the divisor arrives constructively as `succ ap`, matching `div_mod_exec`'s own shape, so no `Lt zero a` hypothesis is formed and no consumer has to discharge one. `Kernel::axiom_footprint` is EMPTY. Admitted by the trusted gate on the first attempt.

Formal statement

theorem Nat.countRange_mul_succ_le_eq_floor : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} AxNat (AxNat.countRange (fun (x3 : AxNat) => AxNat.ble (AxNat.mul (AxNat.succ x0) (AxNat.succ x3)) x1) x2) (Min.min x2 (AxNat.div x1 (AxNat.succ x0))))))

Dependencies

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

2 direct dependencies 1 direct dependents

Evidence

kernel-Nat.countRange_mul_succ_le_eq_floor

Kind: kernel-term
Status: checked

Supports: Nat.countRange_mul_succ_le_eq_floor 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.countRange_mul_succ_le_eq_floor 2>/dev/null | grep -cE '^Nat\.countRange_mul_succ_le_eq_floor[[: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. Anchored with [[:space:]], never \t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY. Pass ONE name per invocation.

footprint-Nat.countRange_mul_succ_le_eq_floor

Kind: exhaustive-enumeration
Status: checked

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

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.

numeric-floor-corollary

Kind: exhaustive-enumeration
Status: checked

Supports: C3 of the ADR-1290 check script verifies the executable form at 37,820 (a, B, n) triples, and C4 checks that Eisenstein's row count is exactly this lemma over 240 ordered prime pairs.

Checker command

python3 docs/research/09-decisions/adr-1290-floor-count-checks.py

Evidence notes

Exit status depends on the finding: any control behaving other than as recorded exits 1. M8 is recorded as a SURVIVOR and asserted to survive -- dropping the min from the assembled lattice identity is true under the prime hypotheses, because the floor never exceeds n there. That is a fact about primes rather than about counting, so it belongs to the consumer and the lemma stays unconditional.

Provenance

{
  "date": "2026-08-31",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_nat_prelude (crates/axeyum-lean-kernel/src/nat_prelude/floor_count.rs)",
  "source": "formal.statement and axiom_footprint are taken verbatim from the kernel's own rendering (Kernel::render_lean of the admitted declaration type, pinned in floor_count_tests::the_family_states_the_intended_types). depends_on is the direct-theorem column intersected with this ledger's registered facts, supplied by scripts/check-fact-depends-derived.py --fix. Nothing about the statement was hand transcribed; title, statement and the evidence notes were authored (lane eisenstein-floors)."
}