D2
plain-language theorem explainer
Indexed accessor that reads the four integer d-components of a midpoint m² TT kernel certificate. Gravity and Regge-analysis proofs cite it whenever a coupling’s second-difference data must be pulled out of the packed CZ record. The body is a four-way match on Fin 4, returning d0–d3.
Claim. Given a packed kernel certificate $c$ (rational scale plus integer difference tables) and an index $a \in \{0,1,2,3\}$, return the $a$-th second-difference integer of $c$: $D_2(c,0)=c.d_0$, $D_2(c,1)=c.d_1$, $D_2(c,2)=c.d_2$, $D_2(c,3)=c.d_3$.
background
The module holds generated kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus. Certificates are packed as the structure CZ: a rational scale (num/den) together with integer tables for first differences, primed differences, and second differences. Scripted tables use Int foldl and scale-32 arithmetic so that kernel checks stay inside decide (no native_decide).
D2 is the second-difference table accessor, parallel to De and Dep for the other tables. Downstream glue identifies these integers with a coupling’s delta2 field: after toCZ, the four Fin-4 slots of D2 recover c.delta2 a by reflexivity. The same pattern appears in the classical-source and continuum-preflight layers when second-depth readings must be compared componentwise.
proof idea
Definitional, not a proof. The body is a single match on the Fin 4 index, projecting the four named integer fields of the certificate. No lemmas are applied; reduction is by rfl after fin_cases at use sites (as in the glue theorem equating D2 after packing to the coupling’s delta2).
why it matters
Feeds the integer contribution term that multiplies two D2 factors into the midpoint m² TT kernel sum, and the glue lemma that transports D2 across the Coupling-to-CZ packing. Downstream damped-schedule and classical-source results reuse the same name pattern when separating depth-two readings or closing residual-vanishing targets. In the broader gravity stack this is bookkeeping infrastructure for the exact 4D Regge kernel certificates, not a physical forcing step (T0–T8, RCL, or the alpha band are not at stake here).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.