Density of the rationals IS the covering property of the open-ball frame

Identifier: F:top-open-ball-frame-covers-the-real-line
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Every real number lies in a basic open ball of every radius: for each x : CReal and each radius index k there is a rational centre q with x in the ball of centre q and radius 1/(k+1). This is the covering property of Top.ballFrame, the open-ball frame of the real line, and the finding recorded here is that it is not a new theorem. Top.MemBall is written as the two-sided rational sandwich creal/density.rs already uses -- x <= ofRat (q + 1/(k+1)) and ofRat (q - 1/(k+1)) <= x -- rather than as |x - q| < eps, because that module measured that the abs form routes the difference through CReal.add and samples at Bishop's shifted index 2n+1 for no gain. With that encoding the proof term is CReal.density x k and nothing else: the restatement type-checks by delta-beta alone. So the density of Q in R and the covering property of the open-ball frame are the same statement, and the frame's vocabulary was chosen to make that visible rather than to hide it behind a re-derivation.

Formal statement

theorem Top.ball_density : ((x0 : CReal) -> ((x1 : AxNat) -> Exists.{1} Rat (fun (x2 : Rat) => Top.MemBall x0 x2 x1)))

Dependencies

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

0 direct dependencies 1 direct dependents

Evidence

kernel-Top.ball_density

Kind: kernel-term
Status: checked

Supports: Top.ball_density is admitted by the trusted kernel gate with the type recorded in formal.statement, and Kernel::axiom_footprint reports 0 assumed names.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example top_frame_theorem_inventory -- Top.ball_density | grep -cE '^theorem[[:space:]]+Top\.ball_density[[:space:]]+2[[:space:]]+0[[:space:]]'

Evidence notes

The exit status depends on the finding three times over. top_frame_theorem_inventory exits NON-ZERO when the filter matches nothing (asking for a declaration and finding none is a failure, not an empty report) AND when any printed row carries a nonempty axiom footprint. grep -c then exits 1 printing 0 unless the anchored row is present with the recorded binder count and a footprint column of exactly 0. Anchored with [[:space:]], never a backslash-t: in a scripted (GNU) grep that is a literal t, and 68 checkers in this ledger were wrong for exactly that reason. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY: this binary builds creal underneath Top, which overflows the default debug thread stack. Definition rows need --defs and are off by default, so a caller who forgets that reads a false ABSENT rather than a wrong type.

suite-the_ball_radius_must_carry_the_plus_one

Kind: exhaustive-enumeration
Status: checked

Supports: The +1 in the radius is load-bearing, and the check is a REFUSAL rather than a comment: the same CReal.density proof term offered against the degenerate radius Rat.div 1 (Rat.natDivSucc k 0) -- that is 1/k, which divides by zero at k = 0, the very index Top.Frame.sup_const's witness uses -- is refused by Kernel::add_declaration, while the 1/(k+1) form is accepted at the same call site with the same term.

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- top_frame::top_frame_tests::the_ball_radius_must_carry_the_plus_one --test-threads=4 2>&1 | grep -cE '^test result: ok\. 1 passed'

Evidence notes

The `1 passed` is load-bearing: `cargo test -- <filter>` runs ZERO tests and exits 0 when the filter matches nothing, so a rename would turn this checker green while checking nothing. Requiring the exact count is what makes the exit status depend on the finding. --release is mandatory (the creal prelude overflows the debug thread stack); --test-threads=4 keeps the shared build off the OOM ceiling. Mutation MUT-D (2026-09-05) makes the control ignore its `degenerate` flag so both halves ask the same question; it kills exactly this one test of the eleven. Mutation MUT-B changes the radius in the PRELUDE from 1/(k+1) to 1/k and kills all eleven, which is reported as non-discriminating for the reason ADR-1602 section 6 records: one bad declaration poisons the shared build, so the failure count then says nothing about how many things are broken.

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_top_frame_prelude (crates/axeyum-lean-kernel/src/top_frame.rs)",
  "source": "Lane `frame-carrier`, roadmap W2-21, executing ADR-1602's pointfree recommendation and decided in ADR-1643 (docs/research/09-decisions/adr-1643-the-frame-carrier-is-nat-indexed-and-the-ball-index-is-not-a-nat.md). formal.statement is Kernel::render_lean of the declaration's type, taken verbatim from the unfiltered emit of `top_frame_theorem_inventory --defs`; axiom_footprint is that tool's footprint column, which reads Kernel::axiom_footprint."
}