IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearingAudit

   1import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearing
   2
   3/-!
   4# Axiom audit: Wave C2 R3 dynamic structure continuum smearing
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearing
  11
  12#check dynamicStructureProfile
  13#check DynamicWeightedContinuumReach
  14#check continuousOn_dynamicStructureProfile
  15#check concreteDynamicInverseMetric_eq_dynamicStructureProfile
  16#check concreteDynamicInverseMetric_eq_sample
  17#check dynamic_weighted_continuum_reach
  18#check background_weighted_reach_misses_dynamic_family
  19#check no_fixed_profile_equals_all_dynamic_profiles
  20#check TypedResidual_gap5_dynamic_continuum_smearing
  21#check typedResidual_gap5_dynamic_continuum_smearing
  22
  23#print axioms continuousOn_dynamicStructureProfile
  24#print axioms concreteDynamicInverseMetric_eq_dynamicStructureProfile
  25#print axioms dynamic_weighted_continuum_reach
  26#print axioms background_weighted_reach_misses_dynamic_family
  27#print axioms no_fixed_profile_equals_all_dynamic_profiles
  28#print axioms typedResidual_gap5_dynamic_continuum_smearing
  29