CoordinateGauss.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The coordinate Gauss identity, proved from Euclidean derivatives and the explicit normal projection. Its right side depends only on the metric.

def OAI.ClosedSurfaceR4.RealModes.inverseMetricPair line 13
Source documentation
Pairing of tangent covectors by the inverse first fundamental form.
```
def inverseMetricPair (E F G a b c d : ℝ) : ℝ :=
…
```
lemma OAI.ClosedSurfaceR4.RealModes.normalPart_dot_normalPart line 16
def OAI.ClosedSurfaceR4.RealModes.coordinateGauss line 33
Source documentation
Gaussian curvature times the coordinate metric determinant.
```
def coordinateGauss (E F G : Base → ℝ) (p : Base) : ℝ :=
…
```
theorem OAI.ClosedSurfaceR4.RealModes.gauss_metric_identity line 43