Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.GeometricFoldVsDictionary4D

show as:
view Lean formalization →

Compares the geometric (edge-origin / distinct-hinge) Regge fold second-variation eigenvalues against the continuum Einstein–Hilbert dictionary on banked TT polarizations at the transverse wavevector symbolDir in 4D. Gravity analysts cite it when separating the true flat Hessian symbol H_fold from mis-transported folds. The argument evaluates both m² sides on axisTTPlus and axisTTCross and records the mismatch certificates.

claimAt the transverse direction $k=\mathrm{symbolDir}$ in 4D Regge calculus on the Freudenthal torus, the geometric-fold mass-squared symbols $m^2_{\mathrm{geom}}$ on the banked TT axes $\mathrm{axisTTPlus}$ and $\mathrm{axisTTCross}$ are computed alongside the continuum dictionary symbols $m^2_{\mathrm{dict}}$ (normalized so a unit-Frobenius TT wave has continuum value $-|k|^2/8$ or equivalent). The module certifies TT-ness and Frobenius identities at this $k$, evaluates both sides, and records $m^2_{\mathrm{geom}}\neq m^2_{\mathrm{dict}}$ on the plus axis (with decoy-gauge control).

background

Arc 2 of the 4D Regge program asks which discrete second-variation symbol is the continuum Einstein–Hilbert Hessian. From the continuum side alone, ContinuumTTSecondVariation4D gives the phase-averaged curvature second variation on a real transverse-traceless cosine wave:

$$\mathrm{ehFace}(H,k)=-(1/4),|k|^2,|H|_F^2.$$

On the Regge side, at a flat background every deficit vanishes, so Schläfli reduces $S=\sum_h A_h\delta_h$ to the cross term $S''=\sum_h(dA_h)(d\delta_h)$ in squared-length coordinates. The exact-action oracle identifies the true flat Hessian symbol $H_{\mathrm{fold}}$: it annihilates vertex-gauge modes and sends normalized TT on $\mathrm{axisTTPlus}$ / $\mathrm{symbolDir}$ to $-1/4$. The distinct-hinge transported fold mis-transports (t12/t13 gauge residue) and is not that continuum object.

symbolDir is chosen transverse to both banked polarizations (their first two rows and columns vanish), so the large row-identity certificates apply at this direction rather than only at the unit-axis wave.

proof idea

Definition-and-certificate module, not a single theorem. It fixes symbolDir, proves Frobenius normalizations and TT projections for axisTTPlus and axisTTCross at that direction, then evaluates two parallel m² pipelines: dictionary symbols (from the continuum / midpoint-Bloch normalization arc) and geometric-fold symbols (from the edge-origin / distinct-hinge fold). A decoy-gauge geometric evaluation supplies a control mode. Inequality certificates (e.g. geometric ≠ dictionary on the plus axis) are the load-bearing outputs; supporting lemmas are mostly algebraic identities and banked decide-style table facts inherited from the imported symbol modules.

why it matters in Recognition Science

Closes Arc 2 step 8’s comparison between geometric fold and continuum dictionary in 4D: it makes precise that the geometric (distinct-hinge) fold is not the EH continuum symbol, in line with the $H_{\mathrm{fold}}$ oracle verdict upstream. Downstream, FoldMomentNamingLink4D uses this landscape when asking whether a named m² moment is the moment of exactFlatCrossTermFold as a functional of that fold’s own symbol. GeometricFoldVsDictionary4DAudit axiom-audits every declaration here against the base triple. SRSConvergesScope4D reads the comparison when stating what ledger-facing EH convergence claims establish and exclude. Landmark link: continuum coefficient $-1/4$ on normalized TT is the Regge normalization target derived without Regge input.

scope and limits

used by (3)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (36)