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 the delta constructions stay inside the certified analytic and geometric toolkit. Analysts of the native delta calculus cite it when they need a single witness that the layer is closed. The module is mostly structure definitions plus one assembled certificate term.

claimThe module defines a strong-closure certificate for the delta-native calculus: a finite list of named proof entries $e_i$, each recording that a specified delta-native construction (amplitudes, probabilities, cubical boundaries, quotient selection, FRS carrier data, etc.) remains inside the certified analytic and multi-distinction geometric toolkit. The assembled object $\mathsf{StrongClosureCertificate}$ packages those entries; $\delta\text{-native strong closure}$ is the corresponding global witness.

background

Primitive Recognition Calculus builds a native real and analytic layer on top of the Recognition Composition Law and the forced cost $J(x)=(x+x^{-1})/2-1$. The delta-native sublayer treats infinitesimal and finite distinctions, amplitudes, and probabilities as first-class objects, together with cubical chain data and multi-distinction geometry.

Upstream modules supply the raw pieces: delta-reals and generable reals, certified analytic protocols and transformers, completion conservativity, cubical chain complexes and all-dimensional cubical boundaries, delta amplitudes and probabilities, FRS carrier structure, prime-axis coherence, quotient selection and examples, and the objecthood registry. This module does not reprove those facts; it indexes them as named closure entries.

The local setting is bookkeeping for strong closure: every delta-native construction used downstream must already sit inside the certified toolkit, so later analysis can treat the layer as a closed algebra rather than an open-ended construction site.

proof idea

Definition-and-assembly module, not a deep proof development. It introduces a record type for a named proof entry in the strong-closure certificate, a constructor that turns an upstream lemma into such an entry, and a certificate bundle type that holds the finite roster. A single assembled term fills that bundle by pointing at the imported delta, analytic, cubical, quotient, and objecthood results. There is no substantial tactic script beyond packaging; the mathematical work lives in the imported modules.

why it matters in Recognition Science

Delta-native analysis imports this module as its closure witness. Without a single strong-closure certificate, every later native-analytic argument would have to re-cite the full import graph and re-check that amplitudes, probabilities, boundaries, and quotients stay inside the certified class. The certificate is the audit point that the delta layer is algebraically closed under the operations the foundation actually uses, which is a prerequisite for treating native delta calculus as a stable substrate rather than a growing construction site. It sits in the Foundation domain beneath the forcing chain landmarks (J-uniqueness, phi, eight-tick structure) and feeds the analysis layer that reads those structures in delta-native language.

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)