ContinuityFromFiniteDescription
plain-language theorem explainer
ContinuityFromFiniteDescription isolates the continuity requirement for the J-cost function on positive reals as a standalone Prop. Researchers reconstructing ledgers or auditing the regularity seam in Recognition Science cite it when splitting obligations into independent components. The structure consists of a single field asserting continuity on the open interval (0, infinity) with no further proof steps required.
Claim. For a function $J : (0, +∞) → ℝ$, the property that $J$ is continuous on the positive reals.
background
The ClosedObservableFramework module absorbs R1, R2, R5, R6 as definitions and isolates the Regularity Axiom (Phase 6) as the finite-description content of C3. ContinuityFromFiniteDescription extracts the continuity obligation from that seam. It depends on extracted arithmetic, which pulls Peano structure from any realization's identity-step orbit, and on the PrimitiveDistinction theorem that reduces seven independent axioms to four substantive structural conditions plus three definitional facts.
proof idea
The declaration is a bare structure definition with no proof body. It directly names the single field ContinuousOn J (Set.Ioi 0) as the continuity obligation. No lemmas or tactics are invoked; the structure serves only as an interface for downstream bundling.
why it matters
It supplies the continuity component to FiniteDescriptionRegularity, which tracks continuity, convexity, and calibration as separately auditable obligations before folding them back into the legacy RegularityCert. This advances the axiom-closure plan by converting the regularity seam into explicit structure fields. In the broader framework it supports ledger reconstruction while keeping the sole remaining axiom the Regularity Axiom encoding finite-description content of C3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.