Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Complete Ordered Field Prc Real C

ARTICLE 4 claims 4 theorems

Foundation Primitive Recognition Calculus Real Complete Ordered Field Prc Real C

A formal certificate that lists the exact conditions under which a recognition-based number system would become the real numbers.

Verify this page

A conditional certificate

The real numbers are usually built from rational numbers by filling in the gaps. One standard way is to take all sequences of rationals that stay close to themselves, the Cauchy sequences, and declare two such sequences equal when they approach the same limit. The declaration prc_real_complete_ordered_field_conditional_certificate is the Recognition Science version of that construction. It is a formal statement, checked by a machine, that lists the precise conditions under which a number system built from recognition events would behave like the real numbers.

In this framework, a ledger, a discrete record of events, starts as a sequence of rational values. The framework defines what it means for such a sequence to be Cauchy, using the same cost-based distance that appears throughout its calculus. The certificate then states that if certain closure and congruence targets hold, the resulting structure is a complete ordered field. Closure means that adding, negating, or multiplying two Cauchy sequences produces another Cauchy sequence. Congruence means that replacing a sequence with an equivalent one does not change the result of these operations. Completeness means that every Cauchy sequence of representatives has a limit inside the structure.

The certificate is conditional because it does not prove all those targets. It proves some of them: the library shows that negation preserves the Cauchy property and that the equivalence relation respects negation. It also proves that addition is closed and well-defined. But the certificate itself is a statement of the form "if these conditions hold, then the structure is a complete ordered field." It is a theorem, not a definition, and it is a theorem about a conditional implication.

What the certificate does not claim is that the recognition-based number system is the real numbers. It does not assert that the closure and congruence targets are all true. It does not prove that multiplication is closed or that the order relation is well-defined; those are left as separate targets. The certificate is a scaffold, not a finished building. It says exactly what would need to be true for the construction to succeed, and it verifies the parts that are already known.

This matters because it shows the framework is not assuming its own conclusion. The path from a ledger of rationals to a complete ordered field is laid out as a series of checkable claims. Some are proved, some are left open. The certificate is the map of that path, with the proved steps marked and the unproved steps labeled. It is an honest accounting of what the framework has established and what it has not.

THEOREM prc_real_complete_ordered_field_conditional_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean
prc_real_complete_ordered_field_conditional_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean:341 
/-- 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
THEOREM PRCRealCompleteOrderedFieldConditionalCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean
PRCRealCompleteOrderedFieldConditionalCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean:320 
/-- Conditional first complete-ordered-field surface. It records that the
carrier and rational embedding are closed, while algebra/order/completeness are
reduced to named exact targets. -/
structure PRCRealCompleteOrderedFieldConditionalCertificate : Prop where
  carrier : Nonempty PRCRealNullClosed
  rat_embedding : Nonempty (PRCRat → PRCRealNullClosed)
  targets : PRCRealCompleteOrderedFieldTargets
  add_operation_from_targets :
    PRCRealAddClosureTarget →
      PRCRealAddCongruenceTarget →
        Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
  neg_operation_from_targets :
    PRCRealNegClosureTarget →
      PRCRealNegCongruenceTarget →
        Nonempty (PRCRealNullClosed → PRCRealNullClosed)
  mul_operation_from_targets :
    PRCRealMulClosureTarget →
      PRCRealMulCongruenceTarget →
        Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
  strength_tag : StrengthTag.traceClosure = StrengthTag.traceClosure
THEOREM PRCRealNegClosureTarget_proved · PRCRealNegCongruenceTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean
PRCRealNegClosureTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean:194 
/-- 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
PRCRealNegCongruenceTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean:227 
/-- Negation respects null equivalence. -/
theorem PRCRealNegCongruenceTarget_proved :
    PRCRealNegCongruenceTarget := by
  intro u v huv eps heps
  rcases huv eps heps with ⟨N, hN⟩
  refine ⟨N, ?_⟩
  intro n hn
  change PRCRat.lt (PRCJCostDistance (-(u.term n)) (-(v.term n))) eps
  rw [PRCJCostDistance_neg_neg]
  exact hN n hn
THEOREM PRCRealAddClosureTarget_proved · PRCRealAddCongruenceTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean
PRCRealAddClosureTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean:170 
/-- 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)
PRCRealAddCongruenceTarget_proved · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedField.lean:204 
/-- Addition respects null equivalence. -/
theorem PRCRealAddCongruenceTarget_proved :
    PRCRealAddCongruenceTarget := by
  intro u u' v v' huu hvv eps heps
  rcases PRCJCostDistanceTriangleModulusTarget_proved eps heps with
    ⟨delta, hdelta_pos, hdelta⟩
  rcases huu delta hdelta_pos with ⟨Nu, hNu⟩
  rcases hvv delta hdelta_pos with ⟨Nv, hNv⟩
  refine ⟨max Nu Nv, ?_⟩
  intro n hn
  have hnu : Nu ≤ n := le_trans (Nat.le_max_left Nu Nv) hn
  have hnv : Nv ≤ n := le_trans (Nat.le_max_right Nu Nv) hn
  exact hdelta
    ((u.term n) + (v.term n))
    ((u'.term n) + (v.term n))
    ((u'.term n) + (v'.term n))
    (by
      rw [PRCJCostDistance_add_right]
      exact hNu n hnu)
    (by
      rw [PRCJCostDistance_add_left]
      exact hNv n hnv)

What this page does not claim

The certificate proves that the recognition-based number system is the real numbers. The certificate proves that multiplication is closed or that the order relation is well-defined. The certificate is a definition of the real numbers within the framework.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND