hFull
plain-language theorem explainer
Defines the full n-dimensional deformed Hessian metric h_λ as the diagonal of cosh(t_i) plus a rank-one update λ cosh(α·t) α⊗α. Anyone proving non-flatness of the deformed cost geometry, or building its Sherman-Morrison inverse and Riemann components, cites this array. The body is a one-line piecewise formula matching the Hessian of Φ_λ.
Claim. For ambient dimension $n$, vectors $\alpha,t\in\mathbb{R}^n$, scalar $\lambda\in\mathbb{R}$, and indices $i,j\in\{0,\ldots,n-1\}$, set $h_\lambda(i,j)=\delta_{ij}\cosh(t_i)+\lambda\cosh(\alpha\cdot t)\,\alpha_i\alpha_j$. This is the Hessian of $\Phi_\lambda(t)=\sum_i\cosh(t_i)+\lambda(\cosh(\alpha\cdot t)-1)$.
background
The module lifts Theorem 2 (non-flatness of the deformed metric) to arbitrary ambient dimension $n$, parallel to how BlockReduction generalized non-parallelism of the mixed projector. The setting is bare-array Hessian geometry: no Matrix API, no manifold tangent spaces. Coordinates are Vec n (functions Fin n → ℝ), and the weighted pairing is the logarithmic aggregate $\alpha\cdot t=\sum_i\alpha_i t_i$.
The undeformed diagonal $D=\mathrm{diag}(\cosh t_i)$ is the Hessian of $\sum_i\cosh(t_i)$. The deformation adds the rank-one term $\lambda\tilde g$ with $\tilde g_{ij}=\cosh(\alpha\cdot t),\alpha_i\alpha_j$, so $h_\lambda=D+\lambda\tilde g$. This matches the named-$\lambda$ packaging of the Hessian entry used in the curvature bridge and agrees with the two-index Hessian already present in the Hessian module.
Shima's formula for Hessian metrics then builds Riemann from the third derivatives $\beta_{ijk}=\partial_i\partial_j\partial_k\Phi$ and the inverse $h^{ij}$. The present definition is the metric array that inverse and curvature constructions act on.
proof idea
Pure definition: no proof obligations. On the diagonal ($i=j$) the entry is $\cosh(t_i)$ plus the rank-one correction; off-diagonal only the correction $\lambda\cosh(\alpha\cdot t),\alpha_i\alpha_j$ survives. The formula is the componentwise Hessian of $\Phi_\lambda$, written as a bare two-index array for later sum manipulations.
why it matters
This is the metric object the curvature bridge is built around. Downstream, hFull_mul_hInvFull proves the Sherman-Morrison two-sided inverse identity in full dimension $n$ (no TwoSparse hypothesis), and hInvFull_symm records symmetry of that inverse. The third-derivative tensor and Shima Riemann arrays are assembled from it; riemann_beta_numerator_zero then kills spectator summands so a mixed component collapses to the certified negative closed form already known in ScalarCertificates.
Module architecture is explicit: bare arrays and syntactic indices, the same strategy that closed Stage A for the projector. Gravity-side consumers in PhysicalSixTetCubicDirichletInstance thread the deformed metric into full-Regge versus Dirichlet residual and limit statements on the cubic lattice. In the broader RS chain this is the cost-geometry side of non-flatness for the deformed potential, not a forcing-chain (T0–T8) step itself, but the concrete Hessian that makes the curvature certificate computable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.