NonlinearSecondVariation4D
plain-language theorem explainer
Type of candidate nonlinear second-variation sequences on the side-N 4-torus: maps mesh size, integer Bloch mode, and edge-length matrix to a real. Cited by the open Schläfli-elevation proposition that demands some independent S'' match the distinct-hinge fold after the (2/N^4) density weight. Pure type alias; no proof content.
Claim. Let $\mathrm{NonlinearSecondVariation4D}$ be the function type $\mathbb{N}\to\mathrm{IntMode4}\to\mathrm{Mat4}\to\mathbb{R}$: for each torus side $N$, integer 4-mode $m$, and $4\times4$ edge-length matrix $E$, a real second-variation value. It is the placeholder type for independent nonlinear flat second variations $S''$ supplied by Schläfli elevation of the edge-length Regge action.
background
The module builds the 4D torus continuum dictionary for a finite periodic Freudenthal action on side $N=j+3$, with $N^4$ sites and density weight $N^{-4}$. Parallel to the closed 3D path, the bookkeeping identity is $(2/N^4)\cdot(N^4/2)=1$, so once Schläfli elevation and the 4D cell-sum are closed, the canonical finite Hamiltonian equals the distinct-hinge Bloch fold.
$\mathrm{Mat4}$ is the local alias for the preflight $4\times4$ matrix type of edge lengths. $\mathrm{IntMode4}$ indexes integer Bloch modes on the 4-torus. The second-variation object $S''$ is meant to come from elevating the nonlinear edge-length Regge action via the 4D pathwise Schläfli identity, not from tautologically rescaling the already-folded symbol.
Until a concrete elevation is supplied, any Prop that asserts existence of such an $S''$ must quantify over this entire function type.
proof idea
Definitional abbreviation only: the body is the function type $\mathbb{N}\to\mathrm{IntMode4}\to\mathrm{Mat4}\to\mathbb{R}$. No tactics, no lemmas, no computational content. Downstream consumers inhabit or quantify over this type when stating the open Schläfli-elevation claim.
why it matters
Anchors the open 4D Schläfli elevation step in the torus continuum limit. Downstream, NonlinearFlatSecondVariation4D re-exports this type, and SchlafliElevationToDistinctHingeOpen asserts existence of some $S''$ of this type such that for every non-aliased side, $(2/N^4)\cdot S''(N,m,E)$ equals the canonical finite 4D Hamiltonian (the legacy distinct-hinge fold).
That open Prop is the 4D analogue of the closed 3D identity $ttSecondDifference=(2/N^3)\cdot S''$ with cell-sum cancellation to 1. Closing it (via a genuine Schläfli derivation in Regge4DSchlafliSecondVariation, not a decoy rescaling) is required before the action-to-symbol dictionary can identify the continuum limit with the midpoint Bloch symbol. It does not itself flip gap-action recovery; it only supplies the type over which the elevation hypothesis ranges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.