Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal

show as:
view Lean formalization →

Defines closed rational intervals and the basic comparison algebra (width, subset, overlap, nested protocols) used as the carrier for certified real analysis in the primitive recognition calculus. Anyone building interval enclosures, generable reals, or FRS carriers cites this layer. The module is definitional scaffolding plus elementary interval lemmas, not a deep existence proof.

claimA closed rational interval is a pair $[\ell,h]\subset\mathbb{Q}$ with $\ell\le h$. Width is $h-\ell\ge 0$. Subset and overlap are the usual relations on such intervals. A protocol is a nested, monotone sequence of intervals (lower bounds nondecreasing, upper bounds nonincreasing) with consistent cross inequalities, used to enclose a real by rational endpoints.

background

In the Recognition Science foundation stack, certified real quantities are not taken as bare Lean Real values. They are presented by rational interval enclosures that can be refined. This module supplies that presentation layer under PrimitiveRecognitionCalculus.

The central object is a closed rational interval: endpoints in $\mathbb{Q}$ with lower bound at most upper bound. Width is the nonnegative difference of endpoints. Subset and overlap are the standard geometric relations. A protocol packages a nested family of such intervals whose lower sequence is monotone nondecreasing and whose upper sequence is monotone nonincreasing, with the cross inequalities that keep every stage a valid enclosure.

Only Mathlib is imported. Downstream analysis modules treat these intervals as the discrete certificates from which generable reals, FRS carriers, and analytic protocols are built.

proof idea

This is a definition module with elementary supporting lemmas, not a deep argument. It introduces the interval structure, width and nonnegativity, subset and overlap predicates, and the protocol bundle (endpoint projections, endpoint ordering, monotonicity of lowers and uppers, and cross inequalities). Proofs are routine rational arithmetic and order facts; there is no forcing-chain or analytic fixed-point content here.

why it matters in Recognition Science

DeltaReal is the shared interval substrate for the primitive recognition calculus. It is imported by CertifiedAnalyticProtocols, DeltaNativeAnalysis, DeltaNativeStrongClosure, FRSCarrier, GenerableReal, ObjecthoodRegistry, and ValidComparisonExamples. Those modules turn nested rational enclosures into certified analytic statements, native delta analysis, strong closure, and the carrier types used for objecthood and generable reals.

In the broader RS picture this sits below the forcing chain (T5 J-uniqueness, T6 phi, T7 eight-tick, T8 D=3): it does not derive constants, but it is the bookkeeping layer that lets later certified comparisons and mass/ladder numerics be stated with explicit rational bounds rather than opaque reals.

scope and limits

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (40)