SimplicialRefinement
plain-language theorem explainer
SimplicialRefinement packages an original list of cubic hinge data with an extra list of hinges on internal diagonals, each required to satisfy the zero-deficit predicate under a given DeficitAngleFunctional and EdgeLengthField. Researchers proving cubic-to-simplicial equivalence in Regge calculus for Recognition Science ledgers cite this structure to establish action invariance under refinement. The definition is a direct structure declaration whose hinges projection is the one-line concatenation of original and extra lists.
Claim. Let $D$ be a deficit angle functional and $L$ an edge length field. A simplicial refinement of an original list of hinge data consists of an extra list of hinge data such that for every extra hinge $h$, the deficit $D(L,h)$ vanishes.
background
The module establishes the cubic-simplicial equivalence for Recognition Science ledgers by abstracting the Freudenthal triangulation of each 3-cube into six congruent tetrahedra. Original hinges correspond to the cube edges that can carry nonzero deficit, while extra hinges lie on face diagonals and the body diagonal. HingeTrivial is the predicate that the deficit angle functional $D$ applied to edge length field $L$ at hinge $h$ equals zero, so internal hinges contribute nothing to the Regge sum.
proof idea
This is a structure definition. The only computational content is the one-line abbreviation for the hinges projection, which concatenates the original list with the extra list.
why it matters
The structure supplies the key hypothesis for the master diagnostic CubicSimplicialInvarianceCert, which certifies that the J-cost to Regge identification remains identical under cubic or simplicial presentation. It implements the structural invariance needed to address Beltracchi's §5 concern on whether the hypercubic ledger to simplicial Regge passage is content-free. The zero-deficit condition on extra hinges aligns with the Recognition Science forcing chain landmarks T7 (eight-tick octave) and T8 (D=3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.