IndisputableMonolith.Gravity.Analysis.GeometricFoldVsDictionary4DAudit

   1import IndisputableMonolith.Gravity.Analysis.GeometricFoldVsDictionary4D
   2import IndisputableMonolith.Gravity.Analysis.SRSConvergesScope4D
   3
   4/-!
   5# Axiom audit: arc 2 step 8
   6
   7Every declaration of `GeometricFoldVsDictionary4D` printed here.  Expected axiom
   8set throughout is the base triple `[propext, Classical.choice, Quot.sound]`.
   9
  10The dictionary side descends from `exactMidpointBlochM2_eq_neg_eighth_frobenius_tt`,
  11whose coefficient-table certificates are kernel-lifted from banked `Int` `decide`
  12chunks with no `native_decide`.  The geometric side descends from the edge-origin
  13`decide` certificates over `Fin 24 × Fin 10`, also kernel-checked.  Neither side
  14introduces a new axiom, so a clean triple here is a statement about postulates
  15only: the ambient theory still supplies the universe hierarchy, inductive types
  16and their recursors, function and dependent types, definitional reduction, and
  17the `Decidable` instances the `decide` calls consume.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Gravity
  22namespace Analysis
  23namespace GeometricFoldVsDictionary4D
  24
  25#print axioms frobId_axisTTPlus
  26#print axioms frobId_axisTTCross
  27#print axioms waveId_symbolDir
  28#print axioms axisTTPlus_isTT_symbolDir
  29#print axioms axisTTCross_isTT_symbolDir
  30#print axioms dict_m2_axisTTPlus_symbolDir
  31#print axioms dict_m2_axisTTCross_symbolDir
  32#print axioms geom_m2_axisTTPlus_symbolDir
  33#print axioms geom_m2_axisTTCross_symbolDir
  34#print axioms geom_m2_decoyGauge_symbolDir
  35#print axioms geom_ne_dict_axisTTPlus
  36#print axioms geom_ne_dict_axisTTCross
  37#print axioms dict_eq_two_geom_axisTTPlus
  38#print axioms dict_eq_two_geom_axisTTCross
  39#print axioms factor_pinned_axisTTPlus
  40#print axioms factor_pinned_axisTTCross
  41#print axioms factor_one_fails
  42#print axioms factor_four_fails
  43#print axioms doubled_fold_is_the_named_object
  44#print axioms two_distinct_bookkeeping_factors
  45#print axioms ehFace_axisTTPlus_symbolDir
  46#print axioms ehFace_eq_four_times_geom
  47#print axioms reggeFace_between
  48#print axioms vanishing_witness_admits_every_factor
  49#print axioms decoyGauge_admits_every_factor
  50#print axioms tt_witness_is_informative
  51#print axioms banked_coefficient_is_not_the_certificate_value
  52#print axioms the_numerals_coincide
  53#print axioms foldTimesTwoEqDictionaryAtBankedWitnesses_holds
  54#print axioms foldDictionaryFactorDischarged_holds
  55#print axioms convergenceReachesDictionaryNotTheHingeMoment_holds
  56
  57/-- Audit package: the discriminating gate holds and the two refutations that make
  58it discriminating are both present. -/
  59theorem step8_audit_package :
  60    FoldDictionaryFactorDischarged ∧
  61      ConvergenceReachesDictionaryNotTheHingeMoment :=
  62  ⟨foldDictionaryFactorDischarged_holds,
  63    convergenceReachesDictionaryNotTheHingeMoment_holds⟩
  64
  65#print axioms step8_audit_package
  66
  67end GeometricFoldVsDictionary4D
  68
  69namespace SRSConvergesScope4D
  70
  71#print axioms srs_limit_value
  72#print axioms eh_face_value
  73#print axioms srs_limit_is_regge_normalization_times_eh
  74#print axioms srs_limit_ne_eh_face
  75#print axioms mesh_sequence_does_not_converge_to_eh_face
  76#print axioms mesh_sequence_converges_to_the_regge_face
  77#print axioms R1_fails_if_the_moments_read_their_symbols
  78#print axioms the_collision_is_real
  79#print axioms step8ScopedVerdict_holds
  80
  81end SRSConvergesScope4D
  82end Analysis
  83end Gravity
  84end IndisputableMonolith
  85