Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CompletionConservativity

show as:
view Lean formalization →

Defines a completion interface from native data N to display data D, together with certificates for display predicates. Conservativity means every certified display fact already holds on the native side; an artifact is a certified display fact with no native preimage. The module proves identity and product completions are conservative, and packages two headline theorems. Downstream native-analysis and certificate-transfer modules import this interface.

claimA completion is a map from native data $N$ to display data $D$. For a display predicate $P$ with certificates $\mathrm{Cert}$, the completion is conservative for $P$ when every certified instance of $P$ on $D$ already holds on $N$. An artifact is a certified display instance with no native witness. The identity completion is conservative; the product completion is conservative for the product predicate.

background

In the Primitive Recognition Calculus, native data $N$ is the RS-side carrier (ledger ticks, cost values, rung indices), while display data $D$ is what appears after a completion or presentation map. Certificates $\mathrm{Cert}$ are finite witnesses that a display predicate $P$ holds on $D$.

Conservativity is the demand that the completion invents nothing: if a certificate proves $P$ on the display side, the corresponding native fact was already true. The dual notion is an artifact: a certified display fact with empty native preimage. The module equates conservativity with absence of artifacts.

Two concrete completions are built in-module: the identity completion (display equals native) and a product completion that pairs components under a product predicate. Both are shown conservative. The setting is pure interface mathematics over Mathlib; no physics constants are fixed here.

proof idea

Definition-heavy module with short algebraic proofs. Completion, CertificateCovered, ConservativeFor, and ArtifactFor are the core structures and predicates. The equivalence conservative_iff_no_artifact is a direct biconditional from the definitions.

identityCompletion is the trivial map; identity_conservative is immediate because native and display coincide. productCompletion and ProductPredicate lift componentwise; product_conservative reduces to conservativity on each factor. Two headline theorems restate the identity and product results for downstream citation.

why it matters in Recognition Science

This module is the conservativity gate for the Primitive Recognition Calculus. Downstream importers are DeltaNativeAnalysis, DeltaNativeStrongClosure, FiniteCertificateTransfer, and ObjecthoodRegistry: they treat display-side certificates as native facts only after a conservative completion is in hand.

Without conservativity, a completion could smuggle display-only structure into native claims (mass ladder placements, objecthood registry entries, finite certificate transfers). The identity and product cases cover the default embeddings used when native data is already complete or when several native streams are paired. The module sits in Foundation and does not itself invoke T5--T8 or the RCL; it supplies the hygiene lemma those later layers assume when they move between native and display presentations.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (16)