Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealMulBoundedContinuity

show as:
view Lean formalization →

Module packaging eventual boundedness of raw rational ledgers in the Primitive Recognition Calculus, so multiplication on the completed ordered field stays continuous under PRC-native cost control. Analysts reconstructing reals from ledger data cite the targets and the conditional certificate. The argument is interface-level: named targets plus a certificate that bounded continuity yields mul closure and congruence.

claimFor a raw rational ledger in the Primitive Recognition Calculus, eventual PRC-native boundedness is formalized so that $J$-cost distance controls multiplication: if sequences are eventually bounded in the PRC sense, then mul on the completed ordered field is continuous, and the corresponding closure and congruence targets follow from a bounded-continuity certificate.

background

Primitive Recognition Calculus builds analysis from ledger data rather than from a pre-given continuum. The parent layer RealCompleteOrderedField supplies the completed ordered field over rationals; this module adds the boundedness side of multiplication continuity.

Eventual boundedness means a raw rational sequence (or Cauchy data) is eventually trapped in a PRC-controlled bound, not merely classically bounded. The $J$-cost distance (from the Recognition Composition Law and T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) is the native metric that must remain continuous under multiplication.

Sibling targets name the pieces: raw eventual boundedness, Cauchy-sequence eventual boundedness, $J$-cost mul-bounded-continuity, and the derived mul-closure and mul-congruence obligations once bounded continuity is assumed.

proof idea

Interface and certificate module rather than a single closed theorem. It declares targets for raw and Cauchy eventual boundedness and for $J$-cost distance mul-bounded continuity, then packages a conditional certificate: from bounded continuity one obtains the real-mul closure and congruence targets. Downstream modules import the certificate and discharge or refine the targets; no standalone end-to-end proof lives here alone.

why it matters in Recognition Science

Multiplication continuity on the PRC real line is required before Kernel-level recognition calculus can treat products of ledger-derived quantities as continuous operations. The module is imported by PrimitiveRecognitionCalculus.Kernel and by RealBoundednessModulus, which refine modulus-of-boundedness control.

In the broader forcing chain, continuous field operations on the completed ledger support later geometric and physical layers (octave structure, dimension forcing) that assume a well-behaved real arithmetic. The conditional certificate keeps the gap explicit: mul continuity is not smuggled in as a classical axiom but tied to PRC-native eventual bounds.

scope and limits

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)