Encyclopedia Foundation Foundation Primitive Recognition Calculus Real Complete Ordered Field Promoted P

ARTICLE 3 claims 3 theorems

Foundation Primitive Recognition Calculus Real Complete Ordered Field Promoted P

A machine-checked certificate confirms that a primitive internal number system already carries the structure of the real numbers, with full typeclass instances deferred to a later packaging step.

Verify this page

The promotion certificate

The real numbers are the complete ordered field: the number system with addition, multiplication, order, and the property that every bounded set has a least upper bound. Recognition Science builds its mathematics from a primitive internal calculus, and this certificate is a formal checkpoint in that construction. It states that the internal null quotient, the framework's own construction of the real numbers, already has the closed operations and theorem surfaces needed by the current complete ordered-field layer.

The certificate is a theorem in the framework's machine-checked library of formal theorems, proved in the file RealCompleteOrderedFieldPromoted.lean. It is a structure with no fields, which means it is a proposition that holds. The theorem establishes that the internal null quotient is ready to support the complete ordered-field layer, but it does not yet provide the full Mathlib typeclass instances. Those remain a later packaging pass, a separate step in the formalization process.

What this means in practice is that the framework's internal real numbers are not yet plugged into the standard mathematical typeclass hierarchy. The certificate is a milestone, not a final integration. It says the internal construction has the right operations and theorems, but the work of connecting it to the wider library of formal mathematics is still open.

In Recognition Science, this certificate is part of a larger chain that forces constants and dimensions from a single cost function. The real numbers are the stage on which that chain plays out. This certificate is the formal guarantee that the stage is ready, even if the wiring to the standard library is not yet complete.

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 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

The certificate does not claim that the internal real numbers are connected to the standard Mathlib typeclass hierarchy. The certificate does not claim that the complete ordered-field layer is fully implemented, only that the internal null quotient is ready for it.

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