constant_term
plain-language theorem explainer
The n-th term of the constant Cauchy ledger on a PRC rational q is definitionally q, for every index n. Anyone simplifying constant sequences inside the PRC real construction will fire this simp lemma. The proof is pure reflexivity from the definition of the constant constructor.
Claim. For every PRC rational $q$ and every natural number $n$, if $c_q$ denotes the constant Cauchy sequence with value $q$, then the $n$-th term satisfies $(c_q)_n = q$.
background
This sits in the Primitive Recognition Calculus real-construction layer. PRC rationals (PRCRat) are nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator (K4.8). Cauchy ledgers over those rationals are the raw sequences from which PRC reals will be quotiented.
The sibling constructor constant packages a fixed PRC rational as a sequence whose every term is that rational. The ambient module is building the Cauchy completion and the intended null-distance relation: the relation that should become the final real quotient once transitivity is proved from the J-cost distance surface.
Upstream cost machinery (J-cost on recognition events, derived costs of multiplicative recognizers, rung-coarsened totals) supplies the metric surface that will later certify which sequences are Cauchy and which pairs are null-equivalent; this lemma itself is purely sequential bookkeeping.
proof idea
One-line definitional proof: rfl. The constant-sequence constructor is defined so that .term n is literally the seed rational, so the equality holds by reduction with no lemmas required. Marked @[simp] so downstream rewrites discharge term lookups automatically.
why it matters
Constant embeddings of rationals into Cauchy ledgers are the first map in any Cauchy-real construction; without a clean term lemma, every later estimate about constant sequences would reopen the definition. In the Recognition foundation this is the bridge from the already-built PRC rational field into the real layer that will host continuous J-cost geometry.
No downstream theorems yet cite it (used_by is empty), but the module’s next objects—null-equivalence of Cauchy ledgers and the eventual real quotient—depend on being able to treat constant sequences as genuine points. Framework-wise it is scaffolding for the real completion that sits under later forcing and cost arguments, not itself a T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.