Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Complete Ordered Field Promoted

ARTICLE 2 claims 2 theorems

Foundation Primitive Recognition Calculus Real Complete Ordered Field Promoted

A machine-checked certificate confirms that the framework's internal real numbers already carry the operations and theorems of a complete ordered field.

Verify this page

The promoted real numbers

The real numbers are the continuum we use for measuring, comparing, and taking limits. A complete ordered field is a structure with addition, multiplication, an order, and the property that every bounded set has a least upper bound. The classical example is the real number line, and any two complete ordered fields are isomorphic, so there is essentially only one.

In Recognition Science, the framework builds its own real numbers from a primitive recognition calculus, a discrete ledger of recognition events. The framework's library, a machine-checked collection of formal theorems, has now certified that this internal construction already supports the full structure of a complete ordered field. The certificate is a formal statement that the internal null quotient, the equivalence classes of the construction, has the closed operations and theorem surfaces needed for the current layer. This is a matter of internal packaging, not a new mathematical discovery: the operations and theorems were already there, and the certificate records that they are available.

The practical effect is that the framework can use the usual language of real analysis, such as continuity, limits, and completeness, without importing an external copy of the reals. The certificate is a theorem in the library, and it is proved in the machine-checked system. This does not claim that the framework's reals are the only possible ones, nor that the construction is simpler than the classical one. It says that the internal reals are ready for the next layer of the framework.

THEOREM prc_real_complete_ordered_field_promoted_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedFieldPromoted.lean
prc_real_complete_ordered_field_promoted_certificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedFieldPromoted.lean:48 
theorem prc_real_complete_ordered_field_promoted_certificate :
    PRCRealCompleteOrderedFieldPromotedCertificate where
  carrier := ⟨PRCRealNullClosed.ofRat 0⟩
  rat_embedding := ⟨PRCRealNullClosed.ofRat⟩
  add_closure := PRCRealAddClosureTarget_proved
  add_congruence := PRCRealAddCongruenceTarget_proved
  add_operation :=
    ⟨PRCRealNullClosed.addOf
      PRCRealAddClosureTarget_proved
      PRCRealAddCongruenceTarget_proved⟩
  neg_closure := PRCRealNegClosureTarget_proved
  neg_congruence := PRCRealNegCongruenceTarget_proved
  neg_operation :=
    ⟨PRCRealNullClosed.negOf
      PRCRealNegClosureTarget_proved
      PRCRealNegCongruenceTarget_proved⟩
  mul_closure := PRCRealMulClosureTarget_of_bounded_continuity
    PRCCauchySeqEventuallyBoundedTarget_proved
    PRCJCostDistanceMulBoundedContinuityTarget_proved
  mul_congruence := PRCRealMulCongruenceTarget_of_bounded_continuity
    PRCCauchySeqEventuallyBoundedTarget_proved
    PRCJCostDistanceMulBoundedContinuityTarget_proved
  mul_operation :=
    ⟨PRCRealNullClosed.mulOf
      (PRCRealMulClosureTarget_of_bounded_continuity
        PRCCauchySeqEventuallyBoundedTarget_proved
        PRCJCostDistanceMulBoundedContinuityTarget_proved)
      (PRCRealMulCongruenceTarget_of_bounded_continuity
        PRCCauchySeqEventuallyBoundedTarget_proved
        PRCJCostDistanceMulBoundedContinuityTarget_proved)⟩
  order_congruence := PRCRealOrderCongruenceTarget_proved
  representative_completeness := PRCRealCompletenessTarget_proved
  first_pass_certificate := prc_real_complete_ordered_field_conditional_certificate
  product_continuity_certificate := prc_real_product_continuity_certificate
  order_congruence_certificate := prc_real_order_congruence_certificate
  completeness_certificate := prc_real_completeness_sharpened_certificate
  strength_tag := rfl
THEOREM PRCRealCompleteOrderedFieldPromotedCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedFieldPromoted.lean
PRCRealCompleteOrderedFieldPromotedCertificate · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/RealCompleteOrderedFieldPromoted.lean:23 
/-- Promoted Step 10 certificate: the internal null quotient has the closed
operations and theorem surfaces needed by the current complete ordered-field
layer. Full Mathlib typeclass instances remain a later packaging pass. -/
structure PRCRealCompleteOrderedFieldPromotedCertificate : Prop where
  carrier : Nonempty PRCRealNullClosed
  rat_embedding : Nonempty (PRCRat → PRCRealNullClosed)
  add_closure : PRCRealAddClosureTarget
  add_congruence : PRCRealAddCongruenceTarget
  add_operation :
    Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
  neg_closure : PRCRealNegClosureTarget
  neg_congruence : PRCRealNegCongruenceTarget
  neg_operation : Nonempty (PRCRealNullClosed → PRCRealNullClosed)
  mul_closure : PRCRealMulClosureTarget
  mul_congruence : PRCRealMulCongruenceTarget
  mul_operation :
    Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
  order_congruence : PRCRealOrderCongruenceTarget
  representative_completeness : PRCRealCompletenessTarget
  first_pass_certificate : PRCRealCompleteOrderedFieldConditionalCertificate
  product_continuity_certificate : PRCRealProductContinuityCertificate
  order_congruence_certificate : PRCRealOrderCongruenceCertificate
  completeness_certificate : PRCRealCompletenessSharpenedCertificate
  strength_tag : StrengthTag.traceClosure = StrengthTag.traceClosure

What this page does not claim

This does not claim that the framework's real numbers are the only complete ordered field. This does not claim that the framework's construction is simpler or more elegant than the classical one. This does not claim that the full Mathlib typeclass instances are already in place.

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/RealCompleteOrderedFieldPromoted.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