IndisputableMonolith.Gravity.Analysis.ReggeM2KernelDecideProbe4D
Probe module that exercises kernel-level `decide` on the 4D midpoint m² transverse-traceless identity certificates. Gravity analysts use it to confirm that the generated scale-32 integer tables discharge the discrete TT kernel checks without native evaluation. The argument is a thin import-and-decide harness over the certified fold tables from the companion kernel-cert module.
claimIn 4D Regge calculus, the midpoint $m^2$ transverse-traceless (TT) kernel identity is checked by pure kernel `decide` on integer fold tables at scale 32: the discrete TT projector applied to the midpoint mass-squared kernel evaluates identically on the certified finite tables.
background
Recognition Science gravity work includes a discrete Regge sector in which continuum curvature and mass-squared operators are replaced by finite combinatorial kernels on triangulations. The midpoint $m^2$ TT identity asserts that the transverse-traceless projection of the midpoint mass-squared kernel vanishes (or matches a fixed algebraic form) on the discrete degrees of freedom.
The upstream module ReggeExactMidpointM2TTIdentity4DKernelCert supplies generated certificates: integer List.foldl tables at scale 32, produced by scripts/qg/regge_4d_m2_kernel_certs_20260721.py, intended for kernel decide only (no native_decide). This probe module sits one layer above those certificates and asks Lean’s kernel to accept the identity checks directly from the tables.
Local setting is 4D Regge analysis inside the Gravity domain: finite, exact integer arithmetic rather than floating-point or classical continuum PDE arguments.
proof idea
Definition-and-probe structure, not a deep tactic proof. Import the generated 4D midpoint $m^2$ TT kernel certificates; expose the scale-32 fold tables; run kernel decide on the resulting propositional equalities. No native_decide, no analytic continuum limit step. Success means the kernel accepts the certified integer identities as proved.
why it matters in Recognition Science
Closes a machine-checkable gap in the 4D Regge $m^2$ TT pipeline: the identity is not only generated offline but re-checked inside Lean’s kernel. Downstream consumers (none linked yet in the graph) would cite it when assembling larger discrete gravity or quantum-geometry certificates that assume the midpoint TT kernel is identically well-behaved in 4D. It supports the broader RS gravity program by keeping curvature/mass-kernel identities exact and auditably finite, rather than numerical. No forcing-chain (T0–T8) step is discharged here; the module is infrastructure for the Regge analysis layer.
scope and limits
- Does not prove a continuum 4D TT identity; only finite scale-32 integer tables.
- Does not use or authorize native_decide; kernel decide only.
- Does not establish existence or uniqueness of Regge triangulations.
- Does not connect to phi-ladder masses, alpha band, or T0–T8 forcing.
- Does not supply new certificates; only probes the imported generated ones.