IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianBlochSymbolZero4DKernelGlue
Glue layer for the 4D Regge flat-Hessian midpoint Bloch analysis: it defines the rational quartic coefficient from the generated coupling table and bridges that table to the integer kernel certificate. Analysts of the symbol-zero kernel cite it when matching ℚ coefficients to the cleared-denominator Int bank. The module is mostly equational wiring (list sums, denominator lemmas, CZ encodings), not a deep existence proof.
claimFor the exact flat 4D Regge Hessian at midpoint Bloch phase, each coupling row supplies a rational $s=p/q$ and edge displacements $D_e,D_{e'}\in\{0,1\}^4$. The module packages the rational quartic coefficient $q$ (same formula as the symbol-zero $q$-coefficient), the scaled integer contributions after clearing denominators by $16$ (so the $\mathbb{Q}$ coefficient is numerator$/32$), and the equalities that identify table sums with the banked integer coupling list used by the kernel certificate.
background
In the Regge gravity analysis, the exact flat Hessian is evaluated in a midpoint Bloch representation. The data module supplies an auto-generated coupling table: each row is a rational Hessian coupling $s=p/q$, edge displacements $D_e,D_{e'}\in{0,1}^4$, and a doubled midpoint offset $\delta_2=2(\mathrm{mid}e-\mathrm{mid}{e'})$. That table is chunked so Lean stays under maxRecDepth.
The companion kernel-certificate module reuses a banked integer coupling list, clears denominators by scale $16$, and treats the rational quartic coefficient as $q_{\mathrm{num}}/32$. It discharges vanishing of those coefficients by decide only (no native_decide).
This glue module sits between those two: it names the rational quartic coefficient (same formula as SymbolZero's $q$-coefficient), converts displacements and contributions into the CZ/Int encoding, and proves the bookkeeping identities (list sums, membership, division by $32$) needed to read the generated table in the certificate's language.
proof idea
Definition-and-bridge module rather than a single deep theorem. It introduces coupling indices and the rational $q$-coefficient, then a chain of small lemmas: coupling-table list extensionality and sum rewrites; nonzero denominators and natural-division identities; maps $D_e,D_{e'}\mapsto$ CZ encodings; equality of each term with the corresponding $q$-contribution over $32$; and membership transfer from the rational table into the integer coupling list. Those equalities are the only proof content; vanishing itself is left to the imported kernel certificate.
why it matters in Recognition Science
Symbol-zero quartic coefficients in the midpoint Bloch Hessian control the kernel structure of the linearized 4D Regge operator on the flat background. Without a faithful bridge from the generated rational table to the Int-encoded certificate, the decide proof that those coefficients vanish cannot see the physics data. This module is that bridge: it locks the $q$-coefficient formula, the $/32$ scaling, and the list-sum accounting so the kernel certificate applies to the exact flat Hessian table rather than to an ad-hoc integer proxy. In the broader Recognition gravity stack it is infrastructure for the discrete curvature/Hessian analysis that sits under continuum limits and continuum matching, not a forcing-chain (T0–T8) step. No downstream consumers are recorded in the graph yet; the intended parent is the symbol-zero kernel vanishing argument that imports both the data and this glue.
scope and limits
- Does not prove vanishing of the quartic coefficients; that lives in the kernel certificate module.
- Does not derive or regenerate the coupling table; the data module is auto-generated and imported as-is.
- Does not address curved backgrounds, non-midpoint Bloch phases, or dimensions other than 4.
- Does not connect to continuum GR limits, mass ladders, or Recognition forcing T0–T8.
- Does not claim completeness of the kernel basis beyond what the imported certificate decides.
depends on (2)
declarations in this module (17)
-
abbrev
CouplingIdx -
def
qCoeff -
theorem
couplingTable_toList_eq_ofFn -
theorem
sum_couplingTable_eq_toList_sum -
theorem
den_ne_zero -
theorem
nat_div_eq_of_dvd -
theorem
De_toCZ -
theorem
Dep_toCZ -
theorem
qContrib_toCZ_eq -
theorem
term_eq_qContrib_div32 -
theorem
toCZ_mem_couplingZList_of_mem_toList -
theorem
term_eq_qContrib_div32_of_mem -
theorem
foldl_add_eq_add_sum -
theorem
foldl_qContrib_eq_sum_map -
theorem
map_qContrib_div_sum -
theorem
qCoeff_eq_qNum_div32 -
theorem
qCoeff_eq_zero