Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal

show as:
view Lean formalization →

Defines closed rational intervals and the comparison protocols built on them for the primitive recognition calculus. Analysts cite it when they need exact, certificate-friendly bounds before lifting to real or native delta analysis. The module is definitional: interval width, nesting, overlap, and monotone endpoint maps, with only elementary nonnegativity and order lemmas.

claimA closed rational interval is a pair $[\ell,h]\subset\mathbb{Q}$ with $\ell\le h$. Width is $h-\ell\ge 0$. Nested inclusion, overlap, and endpoint-monotone protocols supply the comparison language used to certify real quantities by rational bounds.

background

In the Recognition Science foundation layer, primitive recognition calculus needs a carrier for exact, finitary bounds before any appeal to completed reals. This module supplies that carrier as closed intervals with rational endpoints.

The central object is a closed rational interval: lower and upper bounds in $\mathbb{Q}$ with the standing inequality lower $\le$ upper. Width is the nonnegative difference of the endpoints. Subset and overlap are the usual geometric relations on those intervals. A protocol packages monotone endpoint maps (lower nondecreasing, upper nonincreasing) so successive refinements stay nested and comparable.

Only Mathlib is imported. Downstream native-analysis and generable-real modules treat these intervals as the certificate language for delta-style estimates.

proof idea

This is a definition module, not a theorem development. It introduces the interval structure, width, subset/overlap predicates, and protocol endpoint fields, then records the elementary facts that width is nonnegative, endpoints are ordered, and protocol maps preserve the cross inequality between lower and upper bounds. No deep analytic argument lives here.

why it matters in Recognition Science

The module is the shared substrate for seven PrimitiveRecognitionCalculus importers: CertifiedAnalyticProtocols, DeltaNativeAnalysis, DeltaNativeStrongClosure, FRSCarrier, GenerableReal, ObjecthoodRegistry, and ValidComparisonExamples. Those layers lift rational interval certificates to native delta analysis, strong closure, FRS carriers, and objecthood registries. Without a uniform rational-interval protocol language, the later certified-analytic and generable-real arguments would not share a common comparison type. It sits upstream of the forcing-chain analytic work rather than inside T5–T8 themselves.

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)