product_factor_sq_lt
plain-language theorem explainer
For rationals, if $da^2 < \eta$ and $b^2 < M^2$ with $M > 0$, then $(da\,b)^2 < \eta\, M^2$. Continuity and modulus arguments in the primitive recognition calculus cite this when bounding a product increment by a factor times a squared bound. The proof is elementary gap arithmetic: rewrite the square, expand $\eta M^2 - da^2 b^2$, and close with nlinarith.
Claim. Let $da,b,\eta,M\in\mathbb{Q}$. Suppose $da^2 < \eta$, $b^2 < M^2$, and $M > 0$. Then $(da\cdot b)^2 < \eta\cdot M^2$.
background
This lives in the primitive recognition calculus layer that builds real product continuity from rational estimates. The ambient goal is a modulus of continuity for products of quantities controlled in the J-cost / display distance, so one repeatedly needs to pass from a small squared increment $da^2 < \eta$ and a squared bound $b^2 < M^2$ to a squared product bound.
All four parameters are rationals. $M$ is a positive rational bound (not the recognition structure or ledger matrix that share the name $M$ elsewhere). $\eta$ is a positive rational tolerance (not the Minkowski metric or the constant regular-sequence embedding). The only algebraic ingredients are nonnegativity of squares and positivity of products of positive rationals.
The next lemma in the same module, rational_product_increment_sq_lt, packages this factor bound into a four-variable increment estimate with an explicit $\eta = \rho/(4(1+M^2))$ choice.
proof idea
Record $da^2 \ge 0$ and $b^2 \ge 0$ by mul_self_nonneg. From $M > 0$ get $M^2 > 0$ by mul_pos. The two strict hypotheses give positive gaps $\eta - da^2 > 0$ and $M^2 - b^2 > 0$ via nlinarith.
Form the nonnegative cross term $da^2(M^2 - b^2)$ and the positive term $(\eta - da^2)M^2$. Another nlinarith yields $\eta M^2 - da^2 b^2 > 0$. Rewrite $(da,b)^2 = da^2 b^2$ by ring, substitute, and finish with nlinarith.
why it matters
The sole downstream consumer is rational_product_increment_sq_lt in the same module, which lifts the factor bound to a controlled product increment under a concrete choice of $\eta$ in terms of a target $\rho$ and the bound $M$. That increment lemma is part of the chain toward PRCJCostDistanceMulBoundedContinuityTarget_proved and the real-product continuity certificate for the primitive recognition calculus.
In the broader RS foundation this is bookkeeping, not a forcing step: it does not touch T5–T8, the RCL, or the $\phi$-ladder. It simply keeps rational squared estimates closed under multiplication so later real-completion and continuity certificates can quote a clean product modulus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.