IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedFieldPromoted

   1/-
   2  PrimitiveRecognitionCalculus/RealCompleteOrderedFieldPromoted.lean
   3
   4  Round-trip source:
   5    δ/PRC_Universal_Foundation_Execution_Plan_20260526.html
   6
   7  Spec anchor:
   8    Build Order step 10: promote the proved add, neg, mul, order, and
   9    representative-completeness targets into one complete ordered-field
  10    certificate surface over `PRCRealNullClosed`.
  11
  12  This is a certificate-promotion layer. It does not alias the internal carrier
  13  to Lean `ℝ`; it bundles the theorem surfaces already proved for the PRC null
  14  quotient.
  15-/
  16
  17import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteness
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace PrimitiveRecognitionCalculus
  22
  23/-- Promoted Step 10 certificate: the internal null quotient has the closed
  24operations and theorem surfaces needed by the current complete ordered-field
  25layer. Full Mathlib typeclass instances remain a later packaging pass. -/
  26structure PRCRealCompleteOrderedFieldPromotedCertificate : Prop where
  27  carrier : Nonempty PRCRealNullClosed
  28  rat_embedding : Nonempty (PRCRat → PRCRealNullClosed)
  29  add_closure : PRCRealAddClosureTarget
  30  add_congruence : PRCRealAddCongruenceTarget
  31  add_operation :
  32    Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
  33  neg_closure : PRCRealNegClosureTarget
  34  neg_congruence : PRCRealNegCongruenceTarget
  35  neg_operation : Nonempty (PRCRealNullClosed → PRCRealNullClosed)
  36  mul_closure : PRCRealMulClosureTarget
  37  mul_congruence : PRCRealMulCongruenceTarget
  38  mul_operation :
  39    Nonempty (PRCRealNullClosed → PRCRealNullClosed → PRCRealNullClosed)
  40  order_congruence : PRCRealOrderCongruenceTarget
  41  representative_completeness : PRCRealCompletenessTarget
  42  first_pass_certificate : PRCRealCompleteOrderedFieldConditionalCertificate
  43  product_continuity_certificate : PRCRealProductContinuityCertificate
  44  order_congruence_certificate : PRCRealOrderCongruenceCertificate
  45  completeness_certificate : PRCRealCompletenessSharpenedCertificate
  46  strength_tag : StrengthTag.traceClosure = StrengthTag.traceClosure
  47
  48theorem prc_real_complete_ordered_field_promoted_certificate :
  49    PRCRealCompleteOrderedFieldPromotedCertificate where
  50  carrier := ⟨PRCRealNullClosed.ofRat 0⟩
  51  rat_embedding := ⟨PRCRealNullClosed.ofRat⟩
  52  add_closure := PRCRealAddClosureTarget_proved
  53  add_congruence := PRCRealAddCongruenceTarget_proved
  54  add_operation :=
  55    ⟨PRCRealNullClosed.addOf
  56      PRCRealAddClosureTarget_proved
  57      PRCRealAddCongruenceTarget_proved⟩
  58  neg_closure := PRCRealNegClosureTarget_proved
  59  neg_congruence := PRCRealNegCongruenceTarget_proved
  60  neg_operation :=
  61    ⟨PRCRealNullClosed.negOf
  62      PRCRealNegClosureTarget_proved
  63      PRCRealNegCongruenceTarget_proved⟩
  64  mul_closure := PRCRealMulClosureTarget_of_bounded_continuity
  65    PRCCauchySeqEventuallyBoundedTarget_proved
  66    PRCJCostDistanceMulBoundedContinuityTarget_proved
  67  mul_congruence := PRCRealMulCongruenceTarget_of_bounded_continuity
  68    PRCCauchySeqEventuallyBoundedTarget_proved
  69    PRCJCostDistanceMulBoundedContinuityTarget_proved
  70  mul_operation :=
  71    ⟨PRCRealNullClosed.mulOf
  72      (PRCRealMulClosureTarget_of_bounded_continuity
  73        PRCCauchySeqEventuallyBoundedTarget_proved
  74        PRCJCostDistanceMulBoundedContinuityTarget_proved)
  75      (PRCRealMulCongruenceTarget_of_bounded_continuity
  76        PRCCauchySeqEventuallyBoundedTarget_proved
  77        PRCJCostDistanceMulBoundedContinuityTarget_proved)⟩
  78  order_congruence := PRCRealOrderCongruenceTarget_proved
  79  representative_completeness := PRCRealCompletenessTarget_proved
  80  first_pass_certificate := prc_real_complete_ordered_field_conditional_certificate
  81  product_continuity_certificate := prc_real_product_continuity_certificate
  82  order_congruence_certificate := prc_real_order_congruence_certificate
  83  completeness_certificate := prc_real_completeness_sharpened_certificate
  84  strength_tag := rfl
  85
  86end PrimitiveRecognitionCalculus
  87end Foundation
  88end IndisputableMonolith
  89