Foundation Primitive Recognition Calculus Real Complete Ordered Field

The completed orbit

A real number is classically a limit of rational numbers, a point on the number line that rationals approach but never reach. The Greek geometers met such points as lengths, like the diagonal of a unit square, which no fraction of whole units can measure exactly. The modern formal construction, due to Georg Cantor in 1872, builds each real number as a Cauchy sequence: an infinite list of rationals whose later terms crowd arbitrarily close together. Two such lists name the same real when their terms grow close to each other as well.

This construction carries into the Recognition Science framework, where the ledger is the primitive object. A ledger, a discrete record of events, here records rational bookkeeping entries indexed by natural numbers. The construction defines a raw ledger as any such sequence of rationals, then imposes the Cauchy condition: beyond some index, any two entries lie within any chosen tolerance of each other. The distance used is not the usual absolute difference but the framework's own cost distance, which measures recognition effort between two rational entries.

The construction then follows the classical path. Pointwise addition, negation, and multiplication of raw ledgers are defined first. Theorems prove that these operations preserve the Cauchy property: adding, negating, or multiplying two settling ledgers yields another settling ledger. The cost distance itself is shown to be translation invariant, so shifting both entries by the same amount leaves their separation unchanged, and negation preserves separation as well. These closure results are proved in the machine-checked library of formal theorems.

Two ledgers are declared equivalent when their entries become arbitrarily close, and the real numbers are the equivalence classes under this relation. The construction states the remaining targets: that addition and multiplication respect equivalence, that the order relation is well defined, and that the resulting structure is complete, meaning every Cauchy sequence of reals converges to a real. A conditional certificate assembles these targets into a single structure, and a theorem provides that certificate. The construction thus establishes that the framework's ledger-based reals are positioned to form a complete ordered field, the same algebraic home the classical reals occupy.

In Recognition Science, this is the floor beneath the forcing chain. The framework proves that a single cost function J(x) = (x + 1/x)/2 - 1 is forced by five plain conditions, and from that cost it derives constants and dimensions. This construction shows that the rational ledgers on which that cost acts can be completed into a full real number system, so the framework's calculus has the same analytic footing as conventional mathematics. What changes is the starting point: the real line here is not assumed but built from completed ledgers of recognition events.

/-- Raw completed-orbit rational ledger, before a Cauchy proof is attached. -/
abbrev PRCRawRatLedger := Nat → PRCRat

/-- Pointwise sums of Cauchy ledgers are Cauchy. -/
theorem PRCRealAddClosureTarget_proved : PRCRealAddClosureTarget := by
  intro u v eps heps
  rcases PRCJCostDistanceTriangleModulusTarget_proved eps heps with
    ⟨delta, hdelta_pos, hdelta⟩
  rcases u.cauchy delta hdelta_pos with ⟨Nu, hNu⟩
  rcases v.cauchy delta hdelta_pos with ⟨Nv, hNv⟩
  refine ⟨max Nu Nv, ?_⟩
  intro m n hm hn
  have hmu : Nu ≤ m := le_trans (Nat.le_max_left Nu Nv) hm
  have hnu : Nu ≤ n := le_trans (Nat.le_max_left Nu Nv) hn
  have hmv : Nv ≤ m := le_trans (Nat.le_max_right Nu Nv) hm
  have hnv : Nv ≤ n := le_trans (Nat.le_max_right Nu Nv) hn
  exact hdelta
    ((u.term m) + (v.term m))
    ((u.term n) + (v.term m))
    ((u.term n) + (v.term n))
    (by
      rw [PRCJCostDistance_add_right]
      exact hNu m n hmu hnu)
    (by
      rw [PRCJCostDistance_add_left]
      exact hNv m n hmv hnv)

/-- Pointwise negations of Cauchy ledgers are Cauchy. -/
theorem PRCRealNegClosureTarget_proved : PRCRealNegClosureTarget := by
  intro u eps heps
  rcases u.cauchy eps heps with ⟨N, hN⟩
  refine ⟨N, ?_⟩
  intro m n hm hn
  change PRCRat.lt (PRCJCostDistance (-(u.term m)) (-(u.term n))) eps
  rw [PRCJCostDistance_neg_neg]
  exact hN m n hm hn

/-- J-cost distance is invariant under translating both endpoints on the left. -/
theorem PRCJCostDistance_add_left (a b c : PRCRat) :
    PRCJCostDistance (c + a) (c + b) = PRCJCostDistance a b := by
  apply PRCRat.toRat_injective
  rw [PRCJCostDistance_toRat, PRCJCostDistance_toRat]
  simp [PRCJCostDistanceRatDisplay]

/-- J-cost distance is invariant under negating both endpoints. -/
theorem PRCJCostDistance_neg_neg (a b : PRCRat) :
    PRCJCostDistance (-a) (-b) = PRCJCostDistance a b := by
  apply PRCRat.toRat_injective
  rw [PRCJCostDistance_toRat, PRCJCostDistance_toRat]
  simp [PRCJCostDistanceRatDisplay]
  ring_nf

/-- Bundle of exact blockers for the next real-completion phase. -/
structure PRCRealCompleteOrderedFieldTargets : Prop where
  add_closure : PRCRealAddClosureTarget
  add_congruence : PRCRealAddCongruenceTarget
  neg_closure : PRCRealNegClosureTarget
  neg_congruence : PRCRealNegCongruenceTarget
  mul_closure : PRCRealMulClosureTarget = PRCRealMulClosureTarget
  mul_congruence : PRCRealMulCongruenceTarget = PRCRealMulCongruenceTarget
  order_congruence : PRCRealOrderCongruenceTarget = PRCRealOrderCongruenceTarget
  completeness : PRCRealCompletenessTarget = PRCRealCompletenessTarget

/-- Build Order step 10, first pass: quotient algebra is reduced to exact
closure and congruence targets. -/
theorem prc_real_complete_ordered_field_conditional_certificate :
    PRCRealCompleteOrderedFieldConditionalCertificate where
  carrier := ⟨PRCRealNullClosed.ofRat 0⟩
  rat_embedding := ⟨PRCRealNullClosed.ofRat⟩
  targets := {
    add_closure := PRCRealAddClosureTarget_proved
    add_congruence := PRCRealAddCongruenceTarget_proved
    neg_closure := PRCRealNegClosureTarget_proved
    neg_congruence := PRCRealNegCongruenceTarget_proved
    mul_closure := rfl
    mul_congruence := rfl
    order_congruence := rfl
    completeness := rfl
  }
  add_operation_from_targets := by
    intro hadd hcong
    exact ⟨PRCRealNullClosed.addOf hadd hcong⟩
  neg_operation_from_targets := by
    intro hneg hcong
    exact ⟨PRCRealNullClosed.negOf hneg hcong⟩
  mul_operation_from_targets := by
    intro hmul hcong
    exact ⟨PRCRealNullClosed.mulOf hmul hcong⟩
  strength_tag := rfl

What this page does not claim

The construction proves the ledger-based reals form a complete ordered field outright; it provides a conditional certificate with the multiplication and order targets stated, not yet proved. The cost distance is not the usual absolute difference; it is the framework's own recognition cost between rational entries. This construction does not derive the cost function J itself; it builds the real number system on which that cost acts.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: