IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealProductContinuity
Module establishing continuity of real multiplication in the J-cost distance of Primitive Recognition Calculus. It converts square-increment bounds on display factors into controlled J-cost increments under products, then packages a proved bounded-continuity target and a certificate. Downstream Kernel and order-congruence layers cite it when products must stay continuous on bounded sets. The argument is elementary comparison of squares plus the upstream boundedness modulus.
claimOn the positive reals equipped with the J-cost distance $d_J$, multiplication is continuous on sets with a uniform bound: if display-square increments of the factors are small enough relative to a modulus from the boundedness layer, then $d_J(xy,x'y')$ is controlled. The module records the comparison lemmas, the proved mul-bounded continuity target, and a certificate object asserting real product continuity for PRC.
background
Primitive Recognition Calculus works with the cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) and the induced distance on positive reals. Products appear already in the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, so any calculus built on $J$ needs a clean continuity statement for $(x,y)\mapsto xy$ in $d_J$.
The module sits on RealBoundednessModulus, which supplies uniform control of display increments on bounded sets. Sibling material here turns square bounds on factor displays into $d_J$-increments for products, including a rational-product special case, then closes a named mul-bounded continuity target.
Notation is real-analytic: square comparisons on display increments, then transfer to $d_J$ via the standard PRC distance-display dictionary.
proof idea
Not a single theorem: a short chain of comparison lemmas. Square-increment hypotheses on displays are rewritten as strict inequalities for product factors; those feed a rational-product increment bound; the display-to-$d_J$ dictionary then yields the mul-bounded continuity target as proved. A certificate constructor packages the target for import by Kernel and RealOrderCongruence. No deep analysis: algebraic square comparisons plus the upstream modulus.
why it matters in Recognition Science
Product continuity is a prerequisite for any PRC kernel that manipulates multiplicative structure (mass ladders, rung arithmetic, composition identities) while staying inside $d_J$-neighborhoods. Kernel imports the module to obtain a certified real product-continuity fact; RealOrderCongruence uses the same control when order and congruence statements must survive multiplication on bounded sets.
In the broader forcing picture this is infrastructure rather than a T0–T8 landmark: it keeps the real model of $J$ compatible with the RCL product terms so later uniqueness and dimension arguments are not blocked by elementary discontinuity. Without the certificate, downstream layers would re-prove ad-hoc product estimates.
scope and limits
- Does not prove uniqueness of J or force phi; only product continuity in d_J.
- Does not treat unbounded sets; relies on the upstream boundedness modulus.
- Does not establish full joint continuity of the RCL bifunctor, only multiplication.
- Does not address discrete eight-tick or D=3 forcing steps.
- Does not supply numerical constants (c, hbar, G, alpha); pure real-analytic control.
used by (2)
depends on (1)
declarations in this module (7)
-
theorem
PRCJCostDistanceIncrementDisplay_lt_of_sq_lt -
theorem
PRCJCostDistance_sq_lt_of_display_lt_delta -
theorem
product_factor_sq_lt -
theorem
rational_product_increment_sq_lt -
theorem
PRCJCostDistanceMulBoundedContinuityTarget_proved -
structure
PRCRealProductContinuityCertificate -
theorem
prc_real_product_continuity_certificate