IndisputableMonolith.Gravity.Analysis.ReggeHinge4DFlatKernelAudit
IndisputableMonolith/Gravity/Analysis/ReggeHinge4DFlatKernelAudit.lean · 37 lines · 0 declarations
show as:
view math explainer →
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