Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel12Audit

show as:
view Lean formalization →

Audit layer for the Regge 4D full periodic-lattice star deficit kernel of incidence type (1,2). It sits on the QG full-theory campaign one step past the type-(1,1) seed orbit and checks the committed Gram-projection and cleared-denominator cosine calculus against the 15-class stencil. Cite it when verifying that the (1,2) kernel stays API-faithful to the Freudenthal incidence layer. Structure is import-and-audit rather than a new derivation.

claimModule-level audit of the 4D Regge star-hinge deficit kernel on the full periodic lattice for incidence type $(1,2)$: consistency checks that the kernel uses the Freudenthal incidence data, the 15-class stencil, and the fixed Gram-projection / cleared-denominator cosine calculus without redefining those APIs.

background

In the discrete gravity campaign, curvature is carried by deficit angles on hinges of a Regge triangulation. The 4D star kernel packages the local deficit contribution of a vertex star on the full periodic lattice, stratified by incidence type. Type $(1,1)$ is the seed orbit; type $(1,2)$ is the next kernel-checked increment.

Upstream, the audited kernel imports the Freudenthal incidence layer, the 15-class stencil, and the committed Gram-projection / cleared-denominator cosine calculus, and is required never to redefine their API. This audit module exists to pin that contract: same incidence data, same stencil classes, same cosine identities, no silent API drift.

The local setting is analysis support for the quantum-gravity full-theory path, not a continuum Einstein-equation derivation. Notation follows the parent kernel: star deficits, Gram projections of edge vectors, and cleared-denominator cosines on the lattice.

proof idea

This is an audit module, not a derivation module. It imports the type-$(1,2)$ star-deficit kernel and organizes consistency or regression checks against the fixed incidence, stencil, and cosine APIs. Expect wrapper lemmas, equality or definitional comparisons, and interface assertions rather than a fresh geometric construction. No independent forcing or continuum limit is proved here.

why it matters in Recognition Science

The QG full-theory campaign advances by kernel-checked increments: after the type-$(1,1)$ seed orbit, the type-$(1,2)$ kernel is the next committed step. An explicit audit module keeps that step honest relative to the Freudenthal incidence layer and the 15-class stencil, so later hinge or curvature assemblies do not inherit a silently altered cosine calculus.

No downstream consumers are wired in the current graph; the module is infrastructure for reviewers and for locking the $(1,2)$ kernel before further orbit types or global assemblies. It does not itself close a forcing-chain landmark (T0–T8) or a continuum limit, but it protects the discrete curvature substrate those later gravity results would use.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.