Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel22Audit

show as:
view Lean formalization →

Audit companion to the type-(2,2) Regge 4D periodic-lattice star deficit kernel. It packages verification and bookkeeping for the full-orbit hinge class that extends the earlier type-(1,1) seed kernel, without redefining incidence or Gram-cosine APIs. Gravity and discrete-QG workers cite it when checking that the (2,2) stencil closes under the campaign's tier tags. Structure is import-and-audit: it leans on the Kernel22 module rather than reproving the calculus.

claimModule-level audit of the Regge 4D full periodic-lattice star deficit kernel of type $(2,2)$: the hinge-class kernel on the Freudenthal incidence layer with the 15-class stencil and Gram-projection cosine calculus, as the next kernel-checked increment after the type-$(1,1)$ seed orbit.

background

In discrete gravity, Regge calculus encodes curvature as deficit angles on hinges of a simplicial complex. The Recognition Science QG campaign builds 4D star-deficit kernels on a periodic lattice, stratified by orbit type under the lattice symmetry.

The upstream module ReggeHinge4DStarKernel22 is the type-$(2,2)$ full-orbit kernel: "QG full-theory campaign, next kernel-checked increment after ReggeHinge4DStarKernel (type (1,1) seed orbit)." It imports the Freudenthal incidence layer, the 15-class stencil, and the Gram-projection cosine calculus, and never redefines their API. Tier tags on that module are binding for the campaign.

This Audit module sits one import above that kernel. Its role is verification and exposure of the (2,2) class for downstream gravity analysis, not a second copy of the geometric calculus.

proof idea

This is a module shell, not a single theorem. It imports the type-(2,2) star-kernel module and organizes audit-facing declarations (status checks, named interfaces, or thin wrappers) against that kernel's API. No independent incidence or Gram-cosine development lives here; argument structure is "import Kernel22, then audit." Concrete lemmas, if any, are one-step applications or status aggregations over the upstream kernel.

why it matters in Recognition Science

In the gravity domain of the monolith, the (2,2) star kernel is the next checked increment after the (1,1) seed orbit in the QG full-theory campaign. An explicit Audit module makes the kernel's closure and tier-tag compliance inspectable without forcing every consumer to re-read the full Kernel22 development.

No downstream used_by edges are recorded yet, so this module is presently a leaf in the dependency graph: it stabilizes the (2,2) hinge class for later continuum or effective-field matching rather than feeding a named parent theorem today. It does not itself force $D=3$ or the eight-tick octave; those live in the foundation forcing chain (T7, T8). Its place is local discrete-QG bookkeeping on Regge hinges.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.