Foundation Primitive Recognition Calculus Completion Conservativity Product Comp

Certifying combined displays

In formal verification, a certificate is a piece of evidence attached to a data value, and a completion is a bridge that turns native data into a display form while carrying those certificates along. The theorem product_completion_headline, proved in the Recognition Science framework's machine-checked library of formal theorems, states a clean compositional fact: if two display predicates are each certificate-covered, then the combined predicate on the pair of displays is also certificate-covered. In plain terms, if you can certify each of two fields separately, you can certify them together as one record.

The proof is short and structural. Given a pair of displays that each satisfy their predicate, the theorem takes the certificate for the first component and the certificate for the second component, and pairs them. The product completion's certificate relation is defined exactly so that a paired certificate works precisely when both component certificates work. This is the theorem product_conservative, and product_completion_headline is the same statement packaged with its hypotheses made explicit.

The practical meaning is that certification composes. A system that verifies a name field and a date field separately can verify a record holding both, without inventing a new kind of certificate. The same pattern extends to finite vectors and finite fields through the function-space completion theorem, which certifies a whole array coordinatewise. The framework models these as display patterns, not as claims about any particular physical system.

In Recognition Science, this result supports the ledger's bookkeeping: a ledger, a discrete record of events, can carry multiple certified attributes per entry. The theorem does not say that every predicate is certifiable, only that certifiability is preserved when combining already-certifiable components. It also does not say anything about what the certificates mean physically, or about the cost function J that drives the framework's other results. Those are separate theorems with their own scopes.

/-- **Product completion headline.** Certificate-preserving completion is stable
under products, so multi-field display objects can be certified componentwise. -/
theorem product_completion_headline
    {N₁ D₁ Cert₁ N₂ D₂ Cert₂ : Type*}
    (C₁ : Completion N₁ D₁ Cert₁) (C₂ : Completion N₂ D₂ Cert₂)
    (P₁ : D₁ → Prop) (P₂ : D₂ → Prop) :
    ConservativeFor C₁ P₁ → ConservativeFor C₂ P₂ →
      ConservativeFor (productCompletion C₁ C₂) (ProductPredicate P₁ P₂) :=
  product_conservative C₁ C₂ P₁ P₂

/-- Conservative completions compose across products: if each component display
predicate descends to a certificate, the product predicate descends to paired
certificates. -/
theorem product_conservative
    {N₁ D₁ Cert₁ N₂ D₂ Cert₂ : Type*}
    (C₁ : Completion N₁ D₁ Cert₁) (C₂ : Completion N₂ D₂ Cert₂)
    (P₁ : D₁ → Prop) (P₂ : D₂ → Prop)
    (h₁ : ConservativeFor C₁ P₁) (h₂ : ConservativeFor C₂ P₂) :
    ConservativeFor (productCompletion C₁ C₂) (ProductPredicate P₁ P₂) := by
  intro d hd
  rcases hd with ⟨hP₁, hP₂⟩
  rcases h₁ d.1 hP₁ with ⟨c₁, hc₁⟩
  rcases h₂ d.2 hP₂ with ⟨c₂, hc₂⟩
  exact ⟨(c₁, c₂), ⟨hc₁, hc₂⟩⟩

/-- **Function-space completion headline.** Certificate-preserving completion is
stable under pointwise finite/function displays, so finite vectors and finite
fields can be certified coordinatewise. -/
theorem function_completion_headline
    {I N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop) :
    ConservativeFor C P →
      ConservativeFor (functionCompletion I N D Cert C) (AllPredicate P) :=
  function_conservative C P

What this page does not claim

The theorem does not claim that every predicate is certifiable, only that certifiability composes. The theorem says nothing about the physical meaning of certificates or about the cost function J. The theorem does not address dependent records where one field's validity depends on another's value.

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/CompletionConservativity.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: