PRCSameTerm
plain-language theorem explainer
Two PRC Cauchy sequences are related by termwise identity when every rational ledger entry agrees. This is the temporary quotient relation used while null-distance transitivity is still open. Anyone building the first internal real carrier cites it. Equivalence is immediate from reflexivity, symmetry, and transitivity of pointwise equality.
Claim. Let $u$ and $v$ be PRC Cauchy sequences (orbit-indexed rational ledgers that are Cauchy in $J$-cost distance). Write $u \sim_{\mathrm{term}} v$ when $u_n = v_n$ as PRC rationals for every natural number $n$.
background
In the Primitive Recognition Calculus, reals are not imported from Lean's ℝ. A PRC Cauchy sequence is a map $n \mapsto$ PRC rational whose $J$-cost distance eventually falls below every positive PRC rational tolerance. The $J$-cost distance is the recognition cost separating two ledger values; it is the metric that makes the Cauchy condition meaningful in this foundation.
The module is assembling a logic-native complete ordered field by quotienting such sequences. The intended final relation is null $J$-cost distance (sequences that become arbitrarily close). That relation needs a triangle lemma that is not yet closed, so the development first installs a strictly stronger carrier relation: literal termwise equality of the underlying rational sequences.
Upstream integer and rational setoids (Grothendieck completion of logic-natives, then field of fractions) already supply the pattern: define a Prop relation, prove Equivalence, package a Setoid, then quotient.
proof idea
The declaration is a one-line definition: universal quantification over indices with propositional equality of term values. The companion lemma PRCSameTerm.equivalence builds an Equivalence by the standard three constructors: reflexivity is rfl at each index; symmetry applies .symm to the pointwise equality; transitivity chains .trans of the two pointwise equalities. No Cauchy hypothesis or $J$-cost estimate is used.
why it matters
This relation is the raw material for PRCSameTermSetoid, documented as "the first internal setoid available without the null-distance triangle lemma" and "intentionally stronger than the final null-distance setoid." That setoid yields the first internal PRC real carrier: a Cauchy-ledger quotient that is not Lean ℝ, while the final quotient target remains recorded separately as the null-distance setoid goal.
In the Recognition foundation stack, this is scaffolding toward a complete ordered field built only from recognition ledgers and $J$-cost, feeding later forcing-chain and constants work that assumes a native real carrier. It does not itself touch T5–T8, RCL, or the mass ladder; it only keeps the real-construction path open while the preferred geometric null-distance relation is unfinished.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.