Pith. sign in

IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernelAudit

IndisputableMonolith/Gravity/Analysis/ReggeHinge4DDihedralKernelAudit.lean · 50 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel
   2
   3/-!
   4# Axiom audit for `ReggeHinge4DDihedralKernel`
   5
   6Every public theorem must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.Analysis.ReggeHinge4DDihedralKernel
  11
  12#print axioms seedFlatSqEdges_simplex0
  13#print axioms seedFlatSqEdges_simplex1
  14#print axioms cos_numForm
  15#print axioms hingeGramDet_flat
  16#print axioms apexDotNum_flat
  17#print axioms apex3NormSqNum_flat
  18#print axioms apex4NormSqNum_flat
  19#print axioms cosDihedral_flat
  20#print axioms cosDihedral_flat_sq
  21#print axioms cosDihedral_flat_pos
  22#print axioms sinDihedral_flat
  23#print axioms hasDerivAt_cosDihedral_slot0
  24#print axioms hasDerivAt_cosDihedral_slot1
  25#print axioms hasDerivAt_cosDihedral_slot2
  26#print axioms hasDerivAt_cosDihedral_slot3
  27#print axioms hasDerivAt_cosDihedral_slot4
  28#print axioms hasDerivAt_cosDihedral_slot5
  29#print axioms hasDerivAt_cosDihedral_slot6
  30#print axioms hasDerivAt_cosDihedral_slot7
  31#print axioms hasDerivAt_cosDihedral_slot8
  32#print axioms hasDerivAt_cosDihedral_slot9
  33#print axioms hasDerivAt_cosDihedral_coord
  34#print axioms angleKernel_eight
  35#print axioms angleKernel_nine
  36#print axioms singleSimplexDeficitKernel_eight
  37#print axioms singleSimplexDeficitKernel_nine
  38#print axioms singleSimplexDeficitKernel_le_seven
  39#print axioms assembleClassKernel_eval
  40#print axioms partialDeficitClassKernel_three
  41#print axioms partialDeficitClassKernel_seven
  42#print axioms partialDeficitClassKernel_eleven
  43#print axioms partialDeficitClassKernel_zero_off
  44#print axioms partialDeficitClassKernel_values
  45#print axioms cosDihedralKernel_nonvacuous
  46#print axioms cosDihedral_uniformScale_decoy
  47#print axioms cosDihedral_homothety_stationary
  48#print axioms partialDeficitClassKernel_swap23
  49#print axioms hinge4DDihedralKernelStatus_flags
  50

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