Every constructed real's representing sequence is regular

Identifier: F:creal-regular
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every constructed real x (a Cauchy sequence of rationals with an explicit modulus, ADR-0512), the representing sequence CReal.seq x satisfies the CReal.Regular predicate: consecutive terms of the sequence stay within the stated 1/n bound of each other. This is the well-formedness condition every CReal carries by construction and every other CReal lemma in this batch relies on to bound how far apart two sequence terms can be.

Formal statement

theorem CReal.regular : ((x0 : CReal) -> CReal.Regular (CReal.seq x0))

Dependencies

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

0 direct dependencies 50 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CReal.regular

Kind: kernel-term
Status: checked

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

Evidence notes

`build_creal_prelude`/`build_cpoint_prelude` admits this theorem through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so a line in this tool's output for the exact name is a machine-checked proof having been admitted. `theorem_dependency_inventory` builds creal/complex/cpoint in one run; it exits non-zero for a named filter that matches nothing, and `grep -c` (never `-q`) independently asserts the exact tab-anchored line is present. `--release` is MANDATORY: building the constructed carriers recurses deep enough in a debug build to overflow the default thread stack (measured on this tree: release exits 0, debug SIGABRTs at 134).

footprint-CReal.regular

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the creal prelude's trusted surface is empty, which bounds CReal.regular

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --include-constructed --require-axiom-free creal

Evidence notes

`nat_axiom_inventory --include-constructed --require-axiom-free creal` builds the creal environment as its own group and reports `creal: axiom=0 opaque=0 quotient=0 total_trusted=0` (re-measured on this tree), covering Axiom, Opaque AND Quotient, not just Declaration::Axiom. This bounds every individual creal theorem's footprint by []. `--include-constructed` is REQUIRED here -- verified: without it the command exits 1 with "\"creal\" is a known prelude but was NOT built this run ... need --include-constructed", rather than a silent pass; this is the standing trap of an empty/absent result reading as a strong negative when the tool was never pointed at the subject. `--release` is ALSO load-bearing here, and this is a bug this batch found in the pre-existing F-creal-add-comm.json-style pattern (which omits it): measured on this tree, `cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --include-constructed --require-axiom-free creal` (no --release) SIGABRTs with 'has overflowed its stack', exit 134 -- the same deep-recursion resource limit already documented for prelude_theorem_inventory and theorem_dependency_inventory, just not previously measured for this tool. `--release` fixes it: exit 0.

Provenance

{
  "date": "2026-08-25",
  "established_by": "axeyum-lean-kernel build_creal_prelude",
  "source": "theorem name and dependency edges from theorem_dependency_inventory; canonical type read via a standalone probe binary depending on axeyum-lean-kernel by path, calling only its public Kernel API (environment(), display_name(), render_lean(), axiom_footprint()) -- crates/ source untouched."
}