IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.MasterCertificate

   1/-
   2  PrimitiveRecognitionCalculus/Factorization/MasterCertificate.lean
   3
   4  Master certificate for the first δ-native factorization/character-theory
   5  implementation pass.
   6-/
   7
   8import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.GoalClosure
   9import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.CoordinateUniqueness
  10import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodFactor
  11import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.PeriodExistence
  12import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.EvenPeriodGap
  13import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Factorization.SubstrateDichotomy
  14
  15namespace IndisputableMonolith
  16namespace Foundation
  17namespace PrimitiveRecognitionCalculus
  18namespace Factorization
  19
  20/-- Current theorem ledger for the factorization character-theory lane. -/
  21structure DeltaFactorizationCharacterTheoryCertificate : Prop where
  22  chart_transition : ChartTransitionCertificate
  23  residue_orbit : ResidueOrbitCertificate
  24  unit_group : UnitGroupCertificate
  25  period_spectrum : PeriodSpectrumCertificate
  26  finite_mul_character : FiniteMulCharacterCertificate
  27  recognition_lower_bound : RecognitionLowerBoundCertificate
  28  physical_period_readout_interface : PhysicalPeriodReadoutCertificate
  29  prime_coordinate_transform_interface : PrimeCoordinateTransformCertificate
  30  goal_closure : GoalClosureCertificate
  31  coordinate_uniqueness : CoordinateUniquenessCertificate
  32  period_factor : PeriodFactorCertificate
  33  period_existence : PeriodExistenceCertificate
  34  even_period_gap : EvenPeriodGapCertificate
  35  substrate_dichotomy : SubstrateDichotomyCertificate
  36
  37theorem delta_factorization_character_theory_certificate :
  38    DeltaFactorizationCharacterTheoryCertificate where
  39  chart_transition := chart_transition_certificate
  40  residue_orbit := residue_orbit_certificate
  41  unit_group := unit_group_certificate
  42  period_spectrum := period_spectrum_certificate
  43  finite_mul_character := finite_mul_character_certificate
  44  recognition_lower_bound := recognition_lower_bound_certificate
  45  physical_period_readout_interface := physical_period_readout_certificate
  46  prime_coordinate_transform_interface := prime_coordinate_transform_certificate
  47  goal_closure := goal_closure_certificate
  48  coordinate_uniqueness := coordinate_uniqueness_certificate
  49  period_factor := period_factor_certificate
  50  period_existence := period_existence_certificate
  51  even_period_gap := even_period_gap_certificate
  52  substrate_dichotomy := substrate_dichotomy_certificate
  53
  54end Factorization
  55end PrimitiveRecognitionCalculus
  56end Foundation
  57end IndisputableMonolith
  58