Foundation Primitive Recognition Calculus Finite Certificate Transfer Conservati

The transfer theorem

The theorem conservative_completion_transfers in the machine-checked library of formal theorems states a precise transfer property. In plain language: if a completion is conservative for a display predicate, then every witness of that predicate descends to a finite certificate. The completion is a structure that associates finite certificates to data points; the predicate is a property that data points may or may not satisfy; conservativity means the completion does not add new witnesses beyond those the predicate already has. The theorem says that under this condition, for every data point satisfying the predicate, there exists a certificate that the completion certifies for that point.

The proof is immediate from the definition of conservativity. The declaration is a theorem, not a definition, and it is proved in the framework's library with no additional axioms. The same argument also yields a companion result: if an obstruction predicate is conservative, then every continuum obstruction has a finite certificate. The two together form the finite-certificate transfer headline, which the library presents as the formal hinge behind the quantized-proof method.

The theorem does not claim that the certificates are sound or faithful. A certificate map in the weak layer only requires that every witness has some certificate; it does not require that a certificate is issued only to genuine witnesses, nor that a certificate determines the datum it certifies. The library explicitly labels this weak notion prover-defeatable. A completion that certifies everything would satisfy the weak condition vacuously, as the theorem everything_certified_not_faithful shows.

The honest layer comes from a stronger structure, the sound faithful cover, which adds three conditions: completeness, soundness, and faithfulness. With those, a countable certificate system forces the witness set to be countable, and therefore no sound faithful cover exists for the real line. That cardinality obstruction is the honest content the weak layer cannot deliver: finite distinction data cannot soundly and faithfully certify the continuum.

/-- If a completion is conservative for a display predicate, every display
predicate witness descends to a finite certificate. -/
theorem conservative_completion_transfers
    {N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop)
    (hC : ConservativeFor C P) :
    ∀ d : D, P d → ∃ c : Cert, C.certifies c d :=
  hC

/-- If an obstruction predicate is conservative, then every continuum obstruction
has a finite certificate. -/
theorem obstruction_descends
    {N D Cert : Type*} (C : Completion N D Cert) (Obstruction : D → Prop)
    (hC : ConservativeFor C Obstruction) :
    ∀ d : D, Obstruction d → ∃ c : Cert, C.certifies c d :=
  hC

/-- The vacuity-defeating fact. A completion that "certifies everything" (the
trick that made the weak layer vacuous) cannot be faithful as soon as the
display type has two distinct points. So a `SoundFaithfulCover` is genuinely
constrained. -/
theorem everything_certified_not_faithful
    {N D Cert : Type} (C : Completion N D Cert)
    (htriv : ∀ c d, C.certifies c d) (c0 : Cert)
    {d₁ d₂ : D} (hne : d₁ ≠ d₂) :
    ¬ (∀ c d₁ d₂, C.certifies c d₁ → C.certifies c d₂ → d₁ = d₂) :=
  fun hfaith => hne (hfaith c0 d₁ d₂ (htriv c0 d₁) (htriv c0 d₂))

/-- **Named instance: the real line.** No sound, faithful certificate cover by a
countable certificate system exists for the real line. Finite distinction data
cannot soundly and faithfully certify the continuum. -/
theorem no_sound_faithful_certification_of_reals
    {N Cert : Type} [Countable Cert] (C : Completion N ℝ Cert)
    (cover : SoundFaithfulCover C (fun _ : ℝ => True)) : False :=
  no_soundFaithfulCover_of_uncountable_witnesses reals_uncountable_witnesses cover

What this page does not claim

The theorem does not establish that certificates are sound or faithful, only that witnesses have some certificate. The theorem does not apply to the real line with a sound faithful cover, which is impossible. The theorem does not prove the quantized-proof method itself, only a formal hinge for it.

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