directionalLengthCoefficient
plain-language theorem explainer
Defines the conformal directional length coefficient on edge e: the pairing of a vertex potential η with the vertex–edge incidence derivative, omitting the flat edge-length scale. Gravity and discrete GR workers cite it when matching hinge first variations to incidence data or stating rank/separation of deficit vectors. The body is a plain finite sum over vertices.
Claim. For a 3D triangulation $K$, vertex potential $\eta$, and edge $e$, the directional length coefficient is $\sum_i \partial_{\eta_i}\!\ell_e^{\mathrm{inc}}\,\eta_i$, i.e. the incidence-weighted pairing of $\eta$ against edge $e$, without the constant flat edge-length factor.
background
The module treats the discrete vacuum Einstein equation for the nonlinear Regge action on a 3D triangulation $K$. Vacuum means vanishing deficit at every hinge. For the conformal nonlinear action, one direction of the equivalence is zero deficit plus global Schläfli cancellation; the converse needs a rank/nondegeneracy input on the conformal edge-incidence derivative.
A vertex potential $\eta$ is a real assignment to the vertices of $K$, the conformal direction in which edge lengths are varied. The sibling incidence derivative records how each edge responds to a unit bump at a vertex. The present coefficient contracts that derivative against $\eta$, producing a dimensionless directional stretch of edge $e$.
Downstream compatibility statements stress the normalization split: the geometric hinge measure derivative carries an extra $\sqrt{\ell_e^2}$ factor from the flat background lengths, while this coefficient stays scale-free.
proof idea
Pure definition: evaluate the finite sum $\sum_{i\in V(K)}(\text{vertex–edge incidence derivative at }(e,i))\cdot\eta_i$. No lemmas or tactics; the expression is the contracted incidence row for edge $e$.
why it matters
This scalar is the building block for the discrete first-variation calculus in the module. The compatibility proposition equates the geometric hinge directional derivative to $\sqrt{\ell_e^2}$ times this coefficient (plus a vanishing flat-deficit term). The simplified matching theorem drops that zero term once compatibility is assumed.
Incidence separation is stated as: if a deficit vector $\delta$ pairs to zero against every directional length coefficient, then $\delta=0$. Recovery certificates reconstruct $\delta_e$ from those same pairings. The Regge first-variation structure packages the action derivative at the flat potential as a sum of deficits times these conformal edge directions. Restricted incidence recovery reuses the image of the coefficient map as a separating subspace. In short, it is the dimensionless edge observable through which conformal variations talk to hinge deficits in the discrete vacuum Einstein story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.