PRCRealAddCongruenceTarget
plain-language theorem explainer
Null-equivalent Cauchy ledgers stay null-equivalent after pointwise addition of their raw rational terms. Anyone assembling the real quotient from J-cost Cauchy sequences cites this as the well-definedness obligation for addition on classes. The declaration is pure Prop packaging; a sibling theorem discharges it via the J-cost triangle modulus.
Claim. For all Cauchy sequences $u,u',v,v'$ of PRC rationals: if $u$ is null-equivalent to $u'$ and $v$ is null-equivalent to $v'$, then the pointwise sum of the underlying rational ledgers of $u$ and $v$ is raw-null-equivalent to the pointwise sum of those of $u'$ and $v'$.
background
In the primitive recognition calculus, a Cauchy sequence is an orbit-indexed rational ledger whose J-cost distance eventually falls below every positive PRC rational tolerance. Null equivalence says that two such ledgers have J-cost distance eventually smaller than every positive tolerance; it is the intended kernel of the real quotient once transitivity is available from the J-cost surface.
Raw ledgers forget the Cauchy certificate and keep only the term map. Pointwise addition on raw ledgers is termwise rational sum. Raw null equivalence is the same eventual small-J-cost relation, stated directly on those maps. The local module builds a complete ordered-field surface by packaging exact blockers for closure and congruence of the field operations under that null relation.
proof idea
Definitional packaging only: the body is the universal quantification over four Cauchy sequences, two null-equivalence hypotheses, and the raw-null claim on the pointwise sums of the forgotten term maps. No tactics or lemmas run here. The discharging proof is the sibling theorem that addition respects null equivalence, which applies the proved J-cost triangle-modulus target and the two null hypotheses.
why it matters
This is the exact blocker for additive quotient well-definedness under null distance. It sits in the bundle of exact blockers for the next real-completion phase (add closure, add congruence, neg/mul analogues). The conditional complete-ordered-field certificate and the promoted Step 10 certificate both record it as a named target; the proved sibling fills the add-congruence slot so addition descends to the null quotient. Downstream packaging still separates Mathlib typeclass instances from this internal null-quotient surface. Landmark context: the J-cost (T5 uniqueness) supplies the distance that defines both Cauchy and null equivalence, so congruence is a recognition-native step toward reals rather than a classical metric transplant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.