IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealProductContinuity
Module establishing real-product continuity for J-cost distances in the Primitive Recognition Calculus under a bounded modulus. It supplies comparison lemmas from squared factor increments to product and display-distance increments, then packages a continuity certificate. Kernel and RealOrderCongruence import that certificate. The argument is elementary square-factor estimates lifted to the J-cost display metric.
claimUnder a bounded modulus keeping positive real factors away from $0$ and $\infty$, the $J$-cost distance is continuous for multiplication: if the squared increments of the factors are small enough, the squared increment of the product (and of the associated display distance) lies below any prescribed $\delta>0$. The module records this as a real-product continuity certificate.
background
Primitive Recognition Calculus works with the $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) and the induced cost distance on positive reals. Algebraic operations must be continuous in that distance before rational recognition data can be completed to reals.
The upstream module RealBoundednessModulus supplies a modulus that keeps factors inside a compact subset of $(0,\infty)$. Inside that regime one can compare ordinary squared increments of factors with the squared increment of their product, then pass those bounds to the $J$-cost display distance used by the calculus.
The present module develops exactly those comparison lemmas and packages the resulting mul-bounded continuity statement as a reusable certificate.
proof idea
Elementary square-increment lemmas (product_factor_sq_lt, rational_product_increment_sq_lt) bound how far a product moves when each factor moves a controlled amount. Display-distance comparison lemmas then relate those squared increments to the $J$-cost display metric in both directions. The target PRCJCostDistanceMulBoundedContinuityTarget_proved assembles the estimates into the mul-bounded continuity claim, which is wrapped as PRCRealProductContinuityCertificate and the value prc_real_product_continuity_certificate.
why it matters in Recognition Science
Kernel imports the certificate to obtain a usable continuity kernel for real recognition data. RealOrderCongruence reuses the same control when aligning order and congruence structure on the reals. Both sit in the foundation layer that supports the forcing chain from T5 ($J$-uniqueness) onward: continuous multiplicative structure is required for the cost geometry forced by the Recognition Composition Law to extend cleanly from rationals to reals.
scope and limits
- Does not treat factors near 0 or infinity outside the bounded modulus.
- Does not prove uniqueness or form of J; assumes the cost geometry is already fixed.
- Does not address non-commutative or higher-rank products.
- Does not by itself close the full Kernel continuity package.
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