Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeStrongClosure

show as:
view Lean formalization →

Packages a strong closure certificate for the delta-native layer of Primitive Recognition Calculus: a finite roster of named proof entries that jointly certify analytic, geometric, and quotient-selection obligations. Downstream native analysis imports this bundle rather than re-proving each leaf. The module is mostly structure definitions plus a single assembled certificate term.

claimA strong closure certificate is a finite list of named entries $(e_i)$, each pairing a label with a proved obligation in the delta-native calculus (analytic protocols, cubical boundary identities, amplitude/probability coherence, quotient selection, objecthood registry). The assembled object $\mathsf{StrongClosureCertificate}$ asserts that every required native obligation appears and is discharged.

background

Primitive Recognition Calculus develops a delta-native real layer before classical completion: generable reals, certified analytic protocols and transformers, FRS carriers, prime-axis coherence, multi-distinction geometry, and quotient selection. Related imports supply cubical chain complexes, all-dimensional cubical boundary identities, delta amplitudes and probabilities, and completion-conservativity lemmas.

Strong closure means those leaf obligations are not left scattered. This module introduces a small certificate datatype: each ClosureEntry is a named proof slot; entryOf indexes into the roster; StrongClosureCertificate packages the full list. The intent is bookkeeping that a referee can audit entry-by-entry without reopening the analytic or geometric developments underneath.

proof idea

Definition-and-assembly module rather than a deep new argument. It defines the entry record and the certificate structure, maps each required native obligation to a named slot via entryOf, then builds one term strongClosureCertificate (exported as delta_native_strong_closure) by filling every slot with an already-proved lemma from the imported delta-real, analytic-protocol, cubical-boundary, amplitude/probability, quotient, and objecthood modules. No new analytic estimates are proved here; the work is exhaustive wiring and type-checking of the bundle.

why it matters in Recognition Science

Feeds DeltaNativeAnalysis, which imports this module as the single gate that native-layer reasoning is closed under the listed obligations. In the Recognition foundation stack, that closure sits under the forcing chain and the Recognition Composition Law developments: once delta-native facts are certificate-closed, later analysis can treat analytic transformers, cubical identities, and quotient selection as settled rather than open hypotheses. The module therefore converts a large import fan-in into one auditable object for the native-analysis layer.

scope and limits

used by (1)

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

depends on (24)

Lean names referenced from this declaration's body.

declarations in this module (5)