IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FiniteCertificateTransfer
Finite distinction certificates (finite data plus a regime tag) and the maps that carry them into continuum statements. The module proves that conservative completion transfers certificates and that obstructions descend, then introduces sound-faithful covers and shows they force countable witness sets. Downstream delta-native and quantized-proof modules import this transfer layer. Argument is definitional scaffolding plus short transfer and cardinality lemmas.
claimA typed finite distinction is finite data with a regime tag. A certificate map sends such data to continuum statements; legitimacy means the image is a legitimate continuum claim. Conservative completion transfers certificates and descends obstructions. A sound-faithful cover injects distinctions into certified witnesses; if the witness set is uncountable, no sound-faithful cover exists.
background
Primitive recognition calculus works with finite distinction data before any continuum completion. This module packages that data as a typed finite distinction: finite payload plus a tag naming the distinction regime that produced it.
Upstream sits CompletionConservativity: completing a finite recognition structure to a continuum object must not invent new distinctions or erase existing ones. Certificate maps are the morphisms that push finite certificates into continuum statements; a map is legitimate when every image statement is a legitimate continuum claim in that sense.
The second half introduces sound-faithful covers: covers of a continuum statement by certified finite witnesses that are both sound (every certificate is valid) and faithful (distinct continuum distinctions stay distinct). Countability of the witness set is then forced by injectivity of the cover.
proof idea
Definitions first: typed finite distinctions, certificate maps, legitimate continuum statements, and sound-faithful covers. Transfer lemmas are short: legitimacy of the certificate map plus conservativity of completion yields certificate transfer; the contrapositive gives obstruction descent. Cover lemmas are cardinality arguments: sound-faithful covers inject, hence only countably many witnesses can exist; an uncountable witness set blocks any such cover. No deep analytic work lives here; the module is the transfer and cover interface.
why it matters in Recognition Science
Delta-native analysis and strong closure import this module to move finite certificates into continuum delta statements without inventing distinctions. QuantizedProofMethod uses the same transfer layer so quantized proof obligations stay tied to finite certificates. In the Recognition foundation this is the bridge between discrete certificate data and continuum claims, keeping completion conservative (no new physics from limits alone). It supports later forcing-chain and native-analysis work by guaranteeing that continuum conclusions remain finitely certifiable when a sound-faithful cover exists.
scope and limits
- Does not construct explicit continuum completions; only transfers certificates under assumed conservativity.
- Does not prove existence of sound-faithful covers for concrete physical models.
- Does not bound certificate size or computational complexity of the finite data.
- Does not address non-conservative or non-legitimate completion maps.
- Does not derive mass, alpha, or forcing-chain (T5–T8) identities.
used by (3)
depends on (1)
declarations in this module (14)
-
structure
TypedFiniteDistinction -
structure
CertificateMap -
def
LegitimateContinuumStatement -
theorem
certificateMap_legitimate -
theorem
conservative_completion_transfers -
theorem
obstruction_descends -
theorem
finite_certificate_transfer -
structure
SoundFaithfulCover -
theorem
everything_certified_not_faithful -
theorem
soundFaithfulCover_injects -
theorem
soundFaithfulCover_countable_witnesses -
theorem
no_soundFaithfulCover_of_uncountable_witnesses -
theorem
reals_uncountable_witnesses -
theorem
no_sound_faithful_certification_of_reals