A closed interval of the constructive reals is Bishop-compact

Identifier: F:metric-bishop-compactness-of-a-closed-real-interval
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Bishop's definition of compactness for a metric space is COMPLETE plus TOTALLY BOUNDED -- no open sets, no covers, no finite subcover. Both halves are metric conditions and both are now stated for an arbitrary `Metric` and discharged for the closed interval `[a,b]` of the constructive reals, relativized to the predicate `Metric.Interval a b` because this kernel has no `Subtype` and a subspace here is a predicate on the ambient carrier, not a new carrier (ADR-1602). Total boundedness is the substantive half: at accuracy n the net is `g n i = CReal.min b (a + i/(n+1))` for `i <= B*(n+1)`, where B is any natural bounding `b - a` (from `CReal.archimedean`, whose `Exists` is eliminable because the conclusion is a Prop). The `min` is an obligation rather than a convenience -- `Metric.NetIn` requires every net point to satisfy the predicate, and the rational grid runs past b -- and the covering is an induction on the index bound with one `CReal.lt_cotrans` split per step. Completeness is `Metric.creal_completeOn_interval`: a Cauchy sequence inside `[a,b]` converges, and its limit is still inside `[a,b]`.

Formal statement

theorem Metric.creal_compactOn_interval : ((x0 : CReal) -> ((x1 : CReal) -> ((x2 : CReal.le x0 x1) -> Metric.CompactOn Metric.creal (Metric.Interval x0 x1))))    -- Metric.CompactOn M P := And (Metric.TotallyBoundedOn M P) (Metric.CompleteOn M P); Metric.Interval a b := fun x => And (CReal.le a x) (CReal.le x b)

Dependencies

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

1 direct dependencies 1 direct dependents

Evidence

kernel-Metric.creal_compactOn_interval

Kind: kernel-term
Status: checked

Supports: Metric.creal_compactOn_interval 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 kernel_declaration_projection -- --require-declaration Metric.creal_compactOn_interval | grep -cE '^found[[:space:]]+metric[[:space:]]+theorem[[:space:]]+Metric\.creal_compactOn_interval[[:space:]]+0$'

Evidence notes

The exit status depends on the finding twice over: kernel_declaration_projection exits non-zero when the named declaration is in no constructed prelude's environment, and grep -c then exits 1 printing 0 if the anchored row is absent or its axiom-footprint column is not 0. Anchored with [[:space:]] and 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: this binary builds creal/complex/cpoint/metric, which overflow the default debug thread stack.

suite-every_metric_declaration_is_axiom_free

Kind: exhaustive-enumeration
Status: checked

Supports: Every declaration of the Metric namespace, including this one and the total-boundedness theorem it rests on, has an empty Kernel::axiom_footprint. The test derives its name list from the prelude handle's three name structs and the record's own RecordNames selectors, and a companion test (every_metric_namespace_declaration_is_accounted_for) walks Kernel::environment and fails if any Metric.* declaration is missing from that list -- so the subject comes from the kernel, not from a maintainer's memory.

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- metric::metric_tests::every_metric_declaration_is_axiom_free metric::metric_tests::every_metric_namespace_declaration_is_accounted_for --test-threads=4 2>&1 | grep -cE '^test result: ok\. 2 passed'

Evidence notes

The `2 passed` is load-bearing: `cargo test -- <filter>` runs ZERO tests and exits 0 when a 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.

Provenance

{
  "date": "2026-09-04",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_metric_prelude (crates/axeyum-lean-kernel/src/metric/interval.rs and metric/compactness.rs)",
  "source": "Lane `metric-compactness`, roadmap W2-3, recorded in ADR-1607 (docs/research/09-decisions/adr-1607-the-metric-layer-carries-w2-2-and-w2-3.md). formal.statement is Kernel::render_lean of the declaration's type, taken verbatim from metric_tests::w2_3_interval_types_render's printed output; axiom_footprint is read from Kernel::axiom_footprint, never from a rendered name."
}