Pith. sign in

IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssemblyAudit

IndisputableMonolith/Gravity/Analysis/ReggeFlat4DHessianAssemblyAudit.lean · 105 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
   2
   3/-!
   4# Axiom audit for `ReggeFlat4DHessianAssembly`
   5
   6Every public theorem must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.Analysis.ReggeFlat4DHessianAssembly
  11
  12#print axioms hasDerivAt_heronSq_a
  13#print axioms hasDerivAt_heronSq_b
  14#print axioms hasDerivAt_heronSq_c
  15#print axioms hasDerivAt_hingeArea_a
  16#print axioms hasDerivAt_hingeArea_b
  17#print axioms hasDerivAt_hingeArea_c
  18#print axioms heronSq_t11
  19#print axioms heronSq_t12
  20#print axioms heronSq_t13
  21#print axioms heronSq_t22
  22#print axioms hingeArea_t11
  23#print axioms hingeArea_t12
  24#print axioms hingeArea_t13
  25#print axioms hingeArea_t22
  26#print axioms areaGradA_t11
  27#print axioms areaGradB_t11
  28#print axioms areaGradC_t11
  29#print axioms areaGradA_t12
  30#print axioms areaGradB_t12
  31#print axioms areaGradC_t12
  32#print axioms areaGradA_t13
  33#print axioms areaGradB_t13
  34#print axioms areaGradC_t13
  35#print axioms areaGradA_t22
  36#print axioms areaGradB_t22
  37#print axioms areaGradC_t22
  38#print axioms hasDerivAt_area_t11_a
  39#print axioms hasDerivAt_area_t11_b
  40#print axioms hasDerivAt_area_t11_c
  41#print axioms hasDerivAt_area_t12_a
  42#print axioms hasDerivAt_area_t12_b
  43#print axioms hasDerivAt_area_t12_c
  44#print axioms hasDerivAt_area_t13_a
  45#print axioms hasDerivAt_area_t13_b
  46#print axioms hasDerivAt_area_t13_c
  47#print axioms hasDerivAt_area_t22_a
  48#print axioms hasDerivAt_area_t22_b
  49#print axioms hasDerivAt_area_t22_c
  50#print axioms complement_preserves_edge_mask
  51#print axioms kernel21_eq_kernel12
  52#print axioms kernel31_eq_kernel13
  53#print axioms complement_swaps_type_reexport
  54#print axioms areaCov11_eq_grads
  55#print axioms areaCov12_eq_grads
  56#print axioms areaCov22_eq_grads
  57#print axioms orbitCellCount_eq_classification
  58#print axioms classDot_add
  59#print axioms classDot_smul
  60#print axioms orbitZeroMomQuadratic_eq_bilinear
  61#print axioms trueWeightZeroMomQuadratic_eq_bilinear
  62#print axioms trueWeightZeroMomBilinear_symm
  63#print axioms trueWeightZeroMomBilinear_add_left
  64#print axioms trueWeightZeroMomBilinear_smul_left
  65#print axioms trueWeightZeroMomQuadratic_add
  66#print axioms classCoeff_axisTTPlus_int
  67#print axioms classCoeff_decoyGauge_bit
  68#print axioms kernel11_eq_sign
  69#print axioms kernel12_eq_sign
  70#print axioms kernel13_eq_sign
  71#print axioms kernel22_eq_sign
  72#print axioms signDotAxis_kernel11
  73#print axioms signDotAxis_kernel12
  74#print axioms signDotAxis_kernel13
  75#print axioms signDotAxis_kernel22
  76#print axioms signDotGauge_kernel11
  77#print axioms signDotGauge_kernel12
  78#print axioms signDotGauge_kernel13
  79#print axioms signDotGauge_kernel22
  80#print axioms deficitKernel11_dot_axisTTPlus
  81#print axioms deficitKernel12_dot_axisTTPlus
  82#print axioms deficitKernel13_dot_axisTTPlus
  83#print axioms deficitKernel22_dot_axisTTPlus
  84#print axioms deficitKernel11_dot_decoyGauge
  85#print axioms deficitKernel12_dot_decoyGauge
  86#print axioms deficitKernel13_dot_decoyGauge
  87#print axioms deficitKernel22_dot_decoyGauge
  88#print axioms deficitKernel11_dot_decoyTrace
  89#print axioms deficitKernel12_dot_decoyTrace
  90#print axioms deficitKernel13_dot_decoyTrace
  91#print axioms deficitKernel22_dot_decoyTrace
  92#print axioms deficitKernel11_dot_homothety
  93#print axioms deficitKernel12_dot_homothety
  94#print axioms deficitKernel13_dot_homothety
  95#print axioms deficitKernel22_dot_homothety
  96#print axioms orbitDeficit_dot_axisTTPlus
  97#print axioms orbitDeficit_dot_decoyGauge
  98#print axioms orbitDeficit_dot_decoyTrace
  99#print axioms trueWeightZeroMomQuadratic_axisTTPlus
 100#print axioms trueWeightZeroMomQuadratic_decoyGauge
 101#print axioms trueWeightZeroMomQuadratic_decoyTrace
 102#print axioms trueWeightZeroMomQuadratic_homothety
 103#print axioms trueWeight_kills_gauge_at_zero_momentum
 104#print axioms flat4DHessianAssemblyStatus_flags
 105

source mirrored from github.com/jonwashburn/shape-of-logic