Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CompletionConservativity

show as:
view Lean formalization →

Defines a completion interface from native data to display data, together with certificates for display predicates, and the notion of conservativity (no display-only artifacts). Identity and product completions are shown conservative. Downstream native-analysis and objecthood modules import this to keep display-layer claims faithful to native recognition structure.

claimA completion is a map from native data $N$ to display data $D$ equipped with certificates $\mathrm{Cert}$ for display predicates $P$. The completion is conservative when every display fact is certificate-covered from $N$ (equivalently: it admits no artifact). The identity completion and the product completion are conservative.

background

In the Primitive Recognition Calculus, native data $N$ is the ground-level recognition structure; display data $D$ is what appears after a completion (a presentation or packaging layer). Certificates $\mathrm{Cert}$ witness that a display predicate $P$ is already justified on the native side.

Conservativity means the completion adds no new content: every true display claim is certificate-covered. An artifact is a display-level fact with no native certificate. The module equates conservativity with absence of artifacts, then exhibits two standard completions (identity and product) that meet the criterion.

The setting is foundational bookkeeping for Recognition Science: later native-analysis and objecthood arguments must not smuggle display-only structure into theorems about the native calculus.

proof idea

Definition module with short algebraic lemmas. It introduces the completion interface, certificate coverage, conservativity, and artifacts; proves conservativity iff no artifact; builds the identity and product completions; and records two headline theorems that those completions are conservative. No deep analytic argument: the work is interface design plus direct verification on the two canonical constructions.

why it matters in Recognition Science

Feeds four downstream modules by import: DeltaNativeAnalysis, DeltaNativeStrongClosure, FiniteCertificateTransfer, and ObjecthoodRegistry. Those layers reason about native $\Delta$-structure, strong closure, finite certificate transfer, and objecthood; they need a precise guarantee that display packaging does not invent uncertified facts.

In the Recognition framework this is infrastructure under the forcing chain and the native calculus: before citing display-level predicates in mass, octave, or objecthood arguments, one needs conservativity so that native certificates remain the sole source of truth. The identity and product cases are the baseline completions later transfer and registry results build on.

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)