Pith. sign in

IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernelAudit

IndisputableMonolith/Gravity/Analysis/ReggeHinge4DFlatKernelAudit.lean · 37 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   1import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
   2
   3/-!
   4# Axiom audit: `ReggeHinge4DFlatKernel`
   5
   6`#print axioms` for every public theorem of the 4D Freudenthal hinge
   7incidence / flat-Hessian assembly skeleton.  Expected footprint:
   8`[propext, Classical.choice, Quot.sound]`.
   9-/
  10
  11open IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernel
  12
  13#print axioms vertexMask_start
  14#print axioms vertexMask_end
  15#print axioms localEdgeMask_bounds
  16#print axioms localEdgeClass_mask
  17#print axioms permOf_eq_of_eq
  18#print axioms containsSeedHinge_iff
  19#print axioms seedHinge_simplex_count
  20#print axioms seedHinge_simplices
  21#print axioms simplex0Classes_correct
  22#print axioms simplex1Classes_correct
  23#print axioms simplex0Classes_complete
  24#print axioms simplex1Classes_complete
  25#print axioms seedHingeIncidenceNat_values
  26#print axioms sum_seedHingeIncidenceNat
  27#print axioms seedHingeIncidence_nonvacuous
  28#print axioms swap23Mask_bounds
  29#print axioms seedHingeIncidence_swap23
  30#print axioms seedHingeIncidence_decoy_zero
  31#print axioms hingeBoundary_incidence_pos
  32#print axioms simplex_class_count
  33#print axioms cell_covers_all_classes
  34#print axioms seedOrbitAssembly_decoy_area
  35#print axioms seedOrbitAssembly_support_projection
  36#print axioms hinge4DFlatKernelStatus_flags
  37

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