Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedField

show as:
view Lean formalization →

Defines the real complete ordered field inside Primitive Recognition Calculus by completing raw rational ledgers under a Cauchy relation and null equivalence. Supplies addition, negation, multiplication, and the eventual order, plus right/left invariance of J-cost distance under addition. Downstream continuum and kernel modules import it to force J on the completion and to control real multiplication continuity. The development is definitional scaffolding plus elementary algebraic lemmas, not a deep uniqueness proof.

claimFrom raw rational ledgers (sequences of rationals), impose a Cauchy condition and null equivalence, then equip the quotient with $+$, $-$, $\cdot$, and the eventual order $\le^*$, yielding a complete ordered field. On this structure, the J-cost distance satisfies $d_J(x+a,y+a)=d_J(x,y)$ and $d_J(a+x,a+y)=d_J(x,y)$.

background

Primitive Recognition Calculus builds continuum structure from discrete recognition data rather than assuming $\mathbb{R}$ as a black box. A raw rational ledger is a sequence of rationals recording successive recognition values; the module doc frames it as a completed-orbit ledger before any Cauchy certificate is attached.

The upstream import PRCJCostDistanceIncrementTriangle supplies the J-cost distance and its increment/triangle infrastructure. Recall $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), the unique cost forced by the Recognition Composition Law. Distance built from $J$ is the metric language in which Cauchy and null sequences are stated.

Sibling objects introduce the raw ledger type, the Cauchy predicate, null equivalence (sequences that become arbitrarily cheap in $J$-distance), pointwise field operations lifted to ledgers, and the eventual order. The intended quotient is the real complete ordered field used by later PRC continuum arguments.

proof idea

This is primarily a definition module: raw ledgers, Cauchy and null-equivalence relations, and the lifted ring/order operations are introduced as data. Algebraic lemmas such as right and left translation invariance of J-cost distance are short equational arguments from the upstream distance API and the definitions of ledger addition. No heavy analytic completeness theorem is proved here; completeness is encoded by working with Cauchy ledgers modulo null sequences, ready for downstream use.

why it matters in Recognition Science

The module is the real-arithmetic substrate for Primitive Recognition Calculus. It is imported by Continuum.ForcedJOnCompletion, which forces the J-cost functional onto the completed continuum (the continuum-level counterpart of T5 J-uniqueness in the forcing chain), by Kernel, the PRC kernel assembly, and by RealMulBoundedContinuity, which needs ordered-field multiplication to state bounded continuity.

Without a concrete complete ordered field built from recognition ledgers, one cannot pass from discrete eight-tick and phi-ladder combinatorics to continuum statements about $J$, continuity of multiplication, or later identification of physical constants. The module therefore sits under the foundation layer that feeds continuum forcing rather than under phenomenology.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (31)