Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ReggeTTBlochInterfaceAudit

show as:
view Lean formalization →

Audit module for the Bloch-interface layer of the Regge TT continuum-symbol program. It defines the raw cell stencil (216 summands per periodic cell), phase vectors, buckets, and the radical-bearing coefficient built from the flat-angle Jacobian over square-root edge data. Downstream bucket aggregation and Bloch-convention sidecars import it. Content is mostly definitions plus equality lemmas tying the A2-reduced second variation to the raw stencil and checking a row-0 smoke bucket against a rational weight table.

claimInterface layer for the Regge TT Bloch stencil: a raw cell term is a tetrahedron type with an ordered slot pair; the finite cell sum runs over $6\times 6\times 6=216$ summands. Objects include phase vectors, sign-flip on phases, buckets, rational stencil weights, a canonical finite $H$, the raw stencil and its term map, the reduced A2 second-variation identification with that stencil, and the raw Jacobian coefficient $J_{fg}/(2\sqrt{a^*_f})$ together with a row-0 smoke check that this weight matches a rational table entry.

background

Part of the QG full-theory campaign under the ReggeTTContinuumSymbol program, Crux-1(c), in the Normalization-Gated Schläfli Two-Jet protocol. Upstream Gate A2 (ReggeTTFlatSecondVariation) supplies the Schläfli-reduced flat second variation; Gates A0/A1 fix symbol specification and local existence, and the flat first-derivative structure is reused from ReggeTTDerivativeGate without re-proof.

The module introduces the discrete Bloch-interface vocabulary: tetrahedron types and ordered slot pairs as raw stencil terms; phase vectors and their negation; buckets grouping fiber data; rational stencil weights; and a canonical finite $H$. The physically loaded coefficient is the flat-angle Jacobian $J_{fg}$ divided by twice the square root of the Freudenthal flat edge tuple $a^*_f$. The concrete periodic-cell sum has 216 summands.

This is an audit/interface surface, not a production continuum limit. It records the committed raw stencil transcription so later gates can fold, aggregate, and match conventions without reopening A2.

proof idea

Definition-heavy audit module, not a single theorem. Core objects (RawCellStencilTerm, PhaseVector, Bucket, negPhase, rationalStencilWeight, canonicalFiniteH, raw stencil maps) are introduced as data. The main equalities are identification lemmas: a2_reduced_eq_rawCellStencil ties the Gate-A2 reduced second variation to the raw cell stencil fold; row0Smoke_raw_weight_eq_rational checks that on a designated row-0 smoke bucket the raw Jacobian coefficient equals the corresponding rational stencil weight. No continuum or spectral claims are proved here; the module only freezes the interface algebra that aggregation and convention audits will consume.

why it matters in Recognition Science

Closes the raw Bloch-interface transcription left after Gate A2 so later panel gates have a fixed stencil to fold against. ReggeTTBucketAggregation (Gate C-A2f, Paper C / Pillar 1, Lane C) imports it explicitly to discharge the bucket-fiber aggregation gate this module leaves open: equality of the radical-bearing coefficient $J_{fg}/(2\sqrt{a^*_f})$ to a literal rational table on every bucket and all 36 slot pairs, not only the row-0 smoke case. ReggeTTBlochConventionAudit imports it as a non-production sidecar to audit Bloch conventions against the committed spike transcription; that sidecar notes the interface moment is now a stencil fold rather than a definition wired to spike blocks. In the broader RS gravity stack this is bookkeeping for the discrete TT symbol before continuum and normalization claims, not a forcing-chain (T0–T8) step.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)