Dep
plain-language theorem explainer
Field accessor that turns the packed second-edge displacement integers on a coupling certificate into a map from spacetime index to ℤ. Gravity analysts cite it when building edge-pair couplings and quartic Bloch-symbol coefficients for the exact midpoint m² TT identity in 4D Regge calculus. The body is a four-way match on Fin 4.
Claim. Given a packed coupling certificate $c$ (with integer fields $\mathrm{dep}_0,\ldots,\mathrm{dep}_3$), the second-edge displacement at direction $a\in\{0,1,2,3\}$ is $\mathrm{Dep}(c,a)=\mathrm{dep}_a\in\mathbb{Z}$.
background
This module holds kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge analysis. Certificates are generated offline (scale-32 integer tables) and discharged in Lean by decide only.
The packed record CZ stores one unit-cell edge-pair coupling: a rational scale (num/den), first-edge integer components de0–de3, and second-edge components dep0–dep3. Downstream, the unpacked Coupling type exposes functional fields De, Dep : Fin 4 → ℤ, with Dep documented as the doubled midpoint offset $2(\mathrm{mid}e-\mathrm{mid}{e'})$.
Dep is the projection that rebuilds the second-edge map from the packed integers, so later symbol and Hessian code can index by spacetime direction without unpacking by hand.
proof idea
One-line definition: pattern-match the Fin 4 index and return the corresponding packed field (dep0 through dep3). No lemmas; pure structural projection marked @[inline].
why it matters
Feeds the unpacked Coupling record used throughout the flat Hessian / Bloch-symbol pipeline. Downstream consumers include couplingWeight (half-scale product of the two edge strains), couplingMonomial and qCoeff (quartic zero-momentum symbol coefficients), edgeStrain_mul_edgeStrain, and the kernel-glue map Dep_toCZ.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint $m^2$ TT identity certificates: every quartic contribution to the Bloch symbol is built from products of De and Dep components. It does not itself encode a physical law; it makes the generated integer tables usable as functional edge data in 4D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.