module module moderate

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedField`

Defines the raw rational ledger and its Cauchy completion that yields a complete ordered field of reals for Primitive Recognition Calculus. Recognition theorists cite it when lifting discrete J-cost geometry to continuum statements. The module packages ledger arithmetic, null-equivalence, and eventually-le order before any continuum forcing theorem is stated.

claimA raw completed-orbit rational ledger is a sequence of rationals equipped with J-cost distance; Cauchy and null-equivalence relations on such ledgers produce a complete ordered field whose addition, negation, multiplication, and order are induced by eventually-pointwise operations on representatives.

background

Primitive Recognition Calculus works first with discrete rational data and the J-cost $J(x)=(x+x^{-1})/2-1$. Distance and triangle inequalities for increments of $J$ are already available from the imported PRCJCostDistanceIncrementTriangle layer. This module introduces the raw ledger: an orbit of rationals not yet quotiented by a Cauchy proof.

On that raw type one defines pointwise addition, negation, and multiplication, together with an eventually-$\le$ preorder. Cauchy sequences and a null-equivalence relation (sequences that become arbitrarily close in J-cost distance) are then named so that the quotient can serve as a model of the reals. The construction is the standard Cauchy completion, specialized to the J-metric native to Recognition Science rather than the absolute-value metric alone.

The local setting is foundation-level: no continuum forcing or uniqueness of $J$ is proved here; only the algebraic and order scaffolding needed to speak of a complete ordered field built from recognition ledgers.

proof idea

This is primarily a definition module. It introduces the raw ledger carrier, the Cauchy predicate, null-equivalence, and the induced field and order operations (add, neg, mul, eventually-le). Supporting lemmas establish that J-cost distance is compatible with addition on the left and right. No continuum uniqueness or forcing argument is carried; those appear in downstream modules that import this carrier.

why it matters in Recognition Science

Downstream continuum work imports this module as the real carrier. ForcedJOnCompletion needs a completed field on which to force the J-cost functional equation. Kernel and RealMulBoundedContinuity use the same ordered-field structure for bounded continuity of multiplication and for the recognition kernel on the continuum. In the broader RS forcing chain, a complete ordered field is the ambient object on which T5 (J-uniqueness) and later continuum statements are stated; this module supplies that ambient object from rational ledgers rather than assuming classical $\mathbb{R}$ by fiat.

scope and limits

Does not prove uniqueness of J on the completed field.
Does not construct phi, the eight-tick octave, or D=3.
Does not discharge continuum forcing; only supplies the real carrier.
Does not identify the completion with Mathlib's classical real type.
Does not prove physical mass or coupling formulae.

used by (3)

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.ForcedJOnCompletion module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Kernel module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealMulBoundedContinuity module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCJCostDistanceIncrementTriangle module_import

declarations in this module (31)

abbrev PRCRawRatLedger L23
def PRCRawCauchy L27
def PRCRawNullEquivalent L33
def raw L41
theorem raw_cauchy L44
theorem raw_apply L47
def PRCRawAdd L53
def PRCRawNeg L57
def PRCRawMul L61
def PRCRawEventuallyLe L65
theorem PRCJCostDistance_add_right L72
theorem PRCJCostDistance_add_left L79
theorem PRCJCostDistance_neg_neg L86
def PRCRealAddClosureTarget L94
def PRCRealAddCongruenceTarget L98
def PRCRealNegClosureTarget L108
def PRCRealNegCongruenceTarget L112
def PRCRealMulClosureTarget L119
def PRCRealMulCongruenceTarget L124
def PRCRealOrderCongruenceTarget L134
def PRCRawEventuallyClose L142
def PRCRealRepresentativeCauchy L149
def PRCRealRepresentativeLimit L156
def PRCRealCompletenessTarget L165
theorem PRCRealAddClosureTarget_proved L171
theorem PRCRealNegClosureTarget_proved L195
theorem PRCRealAddCongruenceTarget_proved L205
theorem PRCRealNegCongruenceTarget_proved L228
structure PRCRealCompleteOrderedFieldTargets L310
structure PRCRealCompleteOrderedFieldConditionalCertificate L323
theorem prc_real_complete_ordered_field_conditional_certificate L343