PRCRealMulCongruenceTarget
plain-language theorem explainer
Exact blocker: null-equivalence of PRC Cauchy ledgers is a congruence for pointwise multiplication. If u∼u′ and v∼v′ under null distance, the raw products are raw-null-equivalent. Cited by anyone closing the PRC real quotient or the complete ordered-field certificate. Pure Prop definition; discharged downstream from eventual boundedness plus bounded product continuity.
Claim. For all PRC Cauchy sequences $u,u',v,v'$, if $u$ is null-equivalent to $u'$ and $v$ is null-equivalent to $v'$, then the pointwise products of their underlying raw rational ledgers are raw-null-equivalent (J-cost distance eventually below every positive PRC rational tolerance).
background
In the Primitive Recognition Calculus real-completion layer, reals are built as a null-distance quotient of Cauchy ledgers. A PRC Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually falls below every positive PRC rational tolerance. Null-equivalence says the termwise J-cost distance between two such ledgers is eventually smaller than every positive tolerance; raw null-equivalence is the same predicate on bare ledgers.
Pointwise multiplication of raw ledgers is the candidate product. For that product to descend to the quotient, null-equivalence must be a congruence: equivalent factors must yield equivalent products. The module packages exact blockers for each algebraic and order obligation before promoting a complete ordered-field surface.
Upstream, the Cauchy and null-equivalence surfaces come from RealCauchy; raw multiplication and raw null-equivalence are defined in this module as pointwise operations and the corresponding eventual J-cost smallness predicate.
proof idea
Definition only: the body is the quantified Prop itself (four Cauchy sequences, two null-equivalence hypotheses, conclusion raw-null-equivalence of pointwise products). No tactics or lemmas are applied here. Downstream, the obligation is discharged by a conditional theorem that assumes eventual boundedness of Cauchy sequences and bounded product-continuity of J-cost distance, then constructs the required N and eps estimates from those hypotheses.
why it matters
This is the exact multiplicative congruence blocker in the PRC real-completion phase. It sits in the targets bundle for the conditional complete ordered-field certificate and in the promoted Step 10 certificate that records closed operations on the internal null quotient. Downstream, RealMulBoundedContinuity reduces the target to eventual boundedness plus bounded product-continuity and proves the implication; RealBoundednessModulus and RealProductContinuity close related pieces so only continuity remains. Without this congruence, multiplication does not descend to the null-distance quotient, so the PRC carrier cannot carry a field structure. It is scaffolding for the algebra half of the complete ordered-field surface, not a physics landmark (T5–T8) by itself, but it is required before RS-native constants and mass formulas can sit on a completed real line.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.