- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
The PINN parameterizes perturbations via the 14-dimensional \(\mathfrak {g}_2\) adjoint:
Only 14 functions are learned (not 35).
The trained PINN is evaluated on a grid and FFT identifies dominant modes. Coefficients are rationalized to \(\mathbb {Q}\) within tolerance \(10^{-8}\).
The canonical GIFT G2 metric on \(K_7\) is given by:
3-form (\(35\) components, \(7\) non-zero):
where \(c = (65/32)^{1/14}\).
Metric (\(7 \times 7\) diagonal):
Properties:
\(\det (g) = 65/32\) (exact)
\(\| T\| = 0\) (torsion-free)
\(\mathrm{Hol}(g) = G_2\) (by construction)
For \(\varphi = c \cdot \varphi _0\) and metric \(g_{ij} = \frac{1}{6}\sum _{k,l} \varphi _{ikl}\varphi _{jkl}\):
Standard \(\varphi _0\) gives \(g = I_7\), so \(\det (g) = 1\)
Scaling \(\varphi \mapsto c \cdot \varphi \) gives \(g \mapsto c^2 \cdot g\)
Therefore \(\det (g) \mapsto c^{14} \cdot \det (g)\)
Setting \(c^{14} = 65/32\) yields \(\det (g) = 65/32\)