IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCompleteOrderedFieldPromoted
Promoted Step 10 certificate module: the internal null quotient carries the closed field operations and theorem surfaces required by the complete ordered-field layer of Primitive Recognition Calculus. Downstream Kernel imports this packaging. Full Mathlib typeclass instances are deferred to a later pass; the certificate only asserts the internal surfaces exist and close.
claimThe internal null quotient $Q$ is equipped with the closed arithmetic and order operations, and the theorem surfaces, demanded by the complete ordered-field layer; a promoted certificate records that these surfaces are present. Full Mathlib complete-ordered-field typeclass instances are not yet installed.
background
Primitive Recognition Calculus builds its real line from an internal null quotient rather than from a Mathlib real typeclass stack. Upstream RealCompleteness supplies the completeness layer on that quotient. The present module sits one packaging step above that layer.
A "promoted certificate" here means a named record that the quotient already exposes the closed operations (addition, multiplication, order, inverses where defined) and the theorem surfaces the complete ordered-field API expects. The module does not re-derive completeness; it asserts that the Step 10 interface is closed enough for Kernel to consume.
Sibling names in the module are the certificate type and its inhabitant: a structure packing the promoted claim, and a term witnessing it.
proof idea
This is a certificate packaging module, not a deep derivation. It imports RealCompleteness, assembles the promoted Step 10 certificate structure over the internal null quotient, and exposes the closed operation and theorem surfaces required by the current complete ordered-field layer. Full Mathlib typeclass instance synthesis is explicitly left to a later packaging pass.
why it matters in Recognition Science
Kernel imports this module, so every downstream PRC path that needs a complete ordered field on the internal quotient depends on the certificate being present. In the Recognition foundation stack, Step 10 is the bridge from raw completeness to a usable ordered-field surface without yet committing to Mathlib's full instance graph. The deferred typeclass pass keeps the forcing and recognition calculus independent of Mathlib packaging choices while still giving Kernel a stable API.
scope and limits
- Does not install full Mathlib CompleteOrderedField typeclass instances.
- Does not re-prove real completeness; that lives in RealCompleteness.
- Does not identify the null quotient with Mathlib's ℝ.
- Does not claim uniqueness of the promoted packaging beyond the certificate surface.