trivial_hinge_contribution
plain-language theorem explainer
A hinge datum with vanishing deficit angle under a given edge-length field contributes zero to the Regge action via its area-deficit product. Researchers formalizing the cubic-simplicial equivalence in Recognition Science invoke this when showing that internal refinement hinges can be appended without changing the total sum. The argument substitutes the zero-deficit hypothesis and reduces the product with the ring tactic.
Claim. Let $D$ be a deficit-angle functional, $L$ an edge-length field, and $h$ a hinge datum. If $D$ assigns zero deficit to $h$ under $L$, then the product of the area and deficit assigned to $h$ is zero: $D.area(L,h) · D.deficit(L,h) = 0$.
background
The module establishes structural invariance between the cubic ledger and its simplicial triangulation, addressing Beltracchi §5. Every 3-cube subdivides into six tetrahedra; internal edges carry zero deficit because dihedral angles sum exactly to $2π$, while original cube edges retain their cubic deficits. A DeficitAngleFunctional supplies an area and a deficit angle for each hinge datum from the EdgeLengthField, which records conformal lengths $L_{ij}$ derived from vertex log-potentials. HingeTrivial is the predicate that the deficit vanishes for the supplied field.
proof idea
The proof unfolds the definition of HingeTrivial to obtain the hypothesis that the deficit is zero, rewrites this equality into the goal, and applies the ring tactic to conclude that the area-deficit product vanishes.
why it matters
This elementary identity supports the zero-deficit-hinges-drop-out property required for cubic-simplicial equivalence. It is invoked directly by regge_sum_append_trivial, which states that appending any list of trivial hinges leaves the Regge sum unchanged. In the Recognition framework the result confirms that only the original cube edges contribute to the action, so the cubic ledger and its Freudenthal triangulation yield identical values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.