IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeAnalysis

   1/-
   2  PrimitiveRecognitionCalculus/DeltaNativeAnalysis.lean
   3
   4  Public import surface for the Delta-Native Analysis frontier.
   5
   6  The program: stop deriving more ordinary mathematics and instead solve the
   7  interface between forced discrete distinction and the physical continuum
   8  display. The modules below carry the nine-phase plan that achieve this.
   9
  10  * `DeltaReal`              : ℝδ, the rational-interval refinement protocols whose
  11                               forgetful value recovers the classical real line.
  12  * `GenerableReal`          : the countable finite-generation ontology; the
  13                               anti-smuggling guard separating display from
  14                               generation.
  15  * `CertifiedAnalyticProtocols`: countable certified protocol registries for
  16                               analytic/transcendental operations, avoiding
  17                               continuum-valued function graphs.
  18  * `CertifiedAnalyticTransformers`: richer certified registries with binary
  19                               transformers and unary composition closure.
  20  * `FRSCarrier`             : the F_RS carrier as an explicit finite-description
  21                               syntax, sound into the countable RS field.
  22  * `DeltaRealCalibration`   : calibration from one continuum act; the unit `λ = 1`
  23                               is forced by one named continuum datum, not by
  24                               discrete δ.
  25  * `PrimeAxisCoherence`     : the Prime-Axis Coherence Theorem; independent prime
  26                               axes synchronized into one scale.
  27  * `MultiDistinctionGeometry`: geometry from independent distinction channels;
  28                               commuting channel operators and a square-zero
  29                               boundary.
  30  * `QuotientSelection`      : when a permitted quotient is physically forced; gauge
  31                               from indistinguishability.
  32  * `QuotientExamples`       : phase, separating-gauge, and projective quotient
  33                               examples.
  34  * `ObjecthoodRegistry`     : the periodic table of mathematical objecthood.
  35  * `DeltaProbability`       : probability as rational finite-event protocols,
  36                               not real measures over arbitrary sigma-algebras.
  37  * `DeltaAmplitude`         : finite amplitude data and Born weights; Hilbert
  38                               space remains a display completion.
  39  * `FRSComplexAmplitude`    : finite amplitudes over the finite-description
  40                               scalar carrier F_RS[i], displayed into ℂ.
  41  * `HilbertDisplayCompletion`: finite Hilbert space as a display of native
  42                               F_RS[i] amplitudes.
  43  * `PhysicalOneActCalibration`: physical instrument wrapper for the one-act
  44                               curvature datum that forces the canonical unit.
  45  * `ValidComparison`        : native object -> display object -> observable
  46                               protocol, with bridge-composition validity.
  47  * `ValidComparisonExamples`: real, probability, and Hilbert display bridges.
  48  * `CompletionConservativity`: completion interfaces controlled by finite
  49                               certificates; artifacts are exactly uncertified
  50                               display witnesses.
  51  * `FiniteCertificateTransfer`: the hinge theorem: conservative continuum
  52                               statements and obstructions descend to finite
  53                               certificates. AUDIT (2026-06-01): vacuous as a
  54                               weapon (prover-chosen certificate, identity
  55                               transfer). Use `RealLineNonNativity` for content.
  56  * `RealLineNonNativity`     : the cardinality teeth behind the doctrine. No
  57                               countable distinction-certificate system faithfully
  58                               covers ℝ (`real_not_faithfully_certifiable`); the
  59                               dividing line is exactly countability of the witness
  60                               set, which is why countable-witness targets (Hodge)
  61                               need a finer geometric obstruction instead.
  62  * `QuantizedProofMethod`   : problem audits reduce legitimate displays and
  63                               pathologies to finite certificates.
  64  * `HardProblemCertificateAudits`: concrete certificate inventories and finite
  65                               reductions for the first four hard-problem stubs.
  66  * `CubicalChainComplex`    : chain-complex packaging for the local cubical
  67                               boundary law.
  68  * `AllDimensionalCubicalBoundary`: all-dimensional finite boundary API reducing
  69                               higher second boundaries to 2-face ledgers.
  70  * `DeltaNativeStrongClosure`: capstone certificate bundling every closed
  71                               theorem-schema and audit-schema layer.
  72
  73  All modules: no project-local axioms, no sorry.
  74-/
  75
  76import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal
  77import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.GenerableReal
  78import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CertifiedAnalyticProtocols
  79import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CertifiedAnalyticTransformers
  80import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSCarrier
  81import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration
  82import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PrimeAxisCoherence
  83import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.MultiDistinctionGeometry
  84import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection
  85import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientExamples
  86import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ObjecthoodRegistry
  87import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability
  88import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude
  89import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FRSComplexAmplitude
  90import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.HilbertDisplayCompletion
  91import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PhysicalOneActCalibration
  92import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison
  93import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparisonExamples
  94import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CompletionConservativity
  95import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FiniteCertificateTransfer
  96import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealLineNonNativity
  97import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuantizedProofMethod
  98import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.HardProblemCertificateAudits
  99import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CubicalChainComplex
 100import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.AllDimensionalCubicalBoundary
 101import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeStrongClosure
 102