IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCauchy
Defines the PRC-native path from rationals to reals: a strict order via positive ratio-orbit gaps, a J-cost distance, and Cauchy sequences modulo null equivalence. Analysts reconstructing continuum structure inside Recognition Calculus cite it. The module packages order, square-gap, metric, and Cauchy data as the substrate for the real null setoid and kernel.
claimOn the PRC rationals, set $a < b$ when the positive gap $b-a$ has a positive ratio-orbit representative. Equip gaps with a square-gap measure and a $J$-cost distance $d_J$. A sequence $(q_n)$ is PRC-Cauchy when $d_J(q_m,q_n)\to 0$; constant sequences embed $\mathbb{Q}$; null equivalence identifies sequences that vanish in $d_J$.
background
Primitive Recognition Calculus builds arithmetic before classical reals. The upstream RationalField module supplies the PRC rational field; TraceClosure supplies the ratio-orbit and trace data used to detect positivity without an external ordered field.
This module introduces a PRC-native strict order: $a < b$ means the gap $b-a$ is positive in the sense that some ratio-orbit representative is positive. From gaps one defines a square-gap quantity and the $J$-cost distance (the Recognition cost $J(x)=(x+x^{-1})/2-1$ evaluated on ratio data), with the usual self-zero and symmetry lemmas.
Cauchy sequences are then those for which $J$-distance between tails vanishes. Constant sequences recover rationals; null equivalence is the relation of sequences that are $J$-null, the standard first step toward a real completion.
proof idea
Definition-and-lemma module, not a single theorem. Order is defined via positive ratio-orbit representatives of gaps, with bridge lemmas to the underlying rational comparison. Square-gap and $J$-cost distance are defined next; self-zero and symmetry of $d_J$ are short algebraic checks. PRC-Cauchy sequences, constant embeddings, and null equivalence are then packaged as the types and relations the completion will quotient.
why it matters in Recognition Science
Feeds the real null setoid (RealNullSetoid) and the PRC Kernel: those modules import this file to quotient Cauchy sequences by null equivalence and to expose the continuum-level primitives used later in the forcing and recognition chain. Without a PRC-native Cauchy layer, the framework would have to import classical $\mathbb{R}$ rather than reconstruct it from ratio-orbit positivity and $J$-cost. Sits in Foundation under Primitive Recognition Calculus, upstream of any analysis that needs completed scalars inside RS.
scope and limits
- Does not construct the quotient field of reals; only Cauchy data and null equivalence.
- Does not prove completeness of the eventual real field.
- Does not define arithmetic operations on Cauchy sequences beyond the listed structure.
- Does not connect $d_J$ to the classical absolute-value metric on $\mathbb{Q}$.
- Does not address forcing steps T5–T8 or physical constants.
used by (2)
depends on (2)
declarations in this module (21)
-
def
lt -
theorem
lt_iff_toRat_lt -
theorem
zero_lt_of_positive -
def
PRCSquareGap -
theorem
PRCSquareGap_toRat -
def
PRCJCostDistance -
theorem
PRCJCostDistance_self_zero -
theorem
PRCJCostDistance_symmetric -
structure
PRCCauchySeq -
def
constant -
theorem
constant_term -
def
PRCNullEquivalent -
def
PRCNullDistanceTransitiveTarget -
def
PRCNullDistanceSetoidTarget -
def
PRCSameTerm -
def
PRCSameTermSetoid -
def
PRCReal -
def
ofRat -
def
realCauchyClaim -
structure
PRCRealCauchyCertificate -
theorem
real_cauchy_certificate