StrongClosureCertificate
plain-language theorem explainer
A single record type that packages every closed theorem head on the Delta-native surface as a named proof entry. Parameterized layers appear as functions that return entries once their inputs (registries, completions, bridges) are supplied. Anyone citing Delta-native strong closure uses this type as the certificate shape. There is no proof body: it is a pure structure definition whose fields are later filled by concrete theorems.
Claim. A strong-closure certificate is a record of named proof entries (each a proposition with a proof). Fields cover the real $\Delta$-display, generable carriers, certified analytic protocol and transformer registries, FRS carrier and calibration, prime-axis and multi-distinction geometry, cubical face and all-dimensional cubical audits, quotient selection and examples, objecthood and display-object audits, finite/complex/FRSI amplitude and Hilbert display layers, physical comparison bridges, completion conservativity (product, function, finite certificate transfer), problem-audit reduction, stub-obligation reflexivity, and hard-problem / certified-display / domain-specific analytic audits. Parameterized layers are functions into proof entries.
background
In the Primitive Recognition Calculus, the Delta-native interface is the countable, certificate-first presentation of recognition calculus: protocols, displays, and audits are native objects rather than uncountable analytic graphs. A closure entry is a pair of a proposition and a proof of that proposition: a named theorem head packaged so one certificate can list every closed layer.
Upstream modules supply the ingredients those fields point at. Certified analytic registries are countable stores of constant and unary (or richer binary) protocol transformers; finite expressions evaluate to protocols, never continuum graphs. A completion maps native data to display data with certificates for display predicates, and conservativity says those predicates stay certificate-covered. Spatial dimension $D=3$ (forced by T8/T9) appears in related geometry and lattice-edge constructions under the cubical and multi-distinction audits.
The local module assembles those closed heads into one certificate type so strong closure is non-emptiness of this record, not a scattered conjunction.
proof idea
No proof: the declaration is a structure definition. Each field is a closure entry, or a function into closure entries for parameterized layers (registries, completions, bridges, finite $n$, quotient sets). The sibling strongClosureCertificate later fills every field by wrapping an existing theorem head as an entry (for example the real $\Delta$ forgetful display, generable-carrier operationality, transcendental protocol closure over a registry). The theorem delta_native_strong_closure is then the one-line witness that the certificate type is inhabited.
why it matters
This type is the shape of Delta-native strong closure. Downstream, a concrete inhabitant is built field-by-field, and the strong-closure theorem asserts that the certificate type is nonempty: one Lean certificate bundling every closed theorem and audit layer on the Delta-native surface.
In the Recognition framework this is bookkeeping with teeth. It forces the foundation stack (real $\Delta$-display, generable carriers, certified analytics, FRS/calibration, prime-axis and multi-distinction geometry, quotient selection, objecthood, amplitude/Hilbert displays, comparison bridges, and completion conservativity) to present as a single closed interface rather than an open-ended lemma list. That matches the forcing-chain discipline (T0-T8, including $D=3$) by making native-surface closure a checkable object. It does not derive new physics constants; it certifies that the native calculus layers used toward those derivations are already theorem-closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.