NashTorus witness tests

Statement-level sanity checks for the final theorem

nashTorus : 0 < n → IsPosDefSmoothMetric g → IsInjRealizable g.

The proof is machine-checked; what these tests guard against is definitional drift — the hypothesis or conclusion silently meaning something weaker than intended. Each test is either a positive witness (the hypothesis class is non-empty and non-trivial, the conclusion is attainable by the expected map) or a negative witness (the conclusion is not satisfiable by a degenerate map).

Tests are grouped by what they discriminate:

• N1–N2: nashTorus applies to the flat metric and to a genuinely $x$-dependent metric (2 + sin x₀) · I.
• N3: Realizes is not vacuous — a constant map does not realize the flat metric.
• N4: IsInjectiveEmbedding is not vacuous — the zero map fails it.
• N5: IsInjectiveMod2Pi uses the lattice 2πℤⁿ, not a finer one — the doubled circle map x ↦ (cos 2x, sin 2x) fails it.
• N6: the flat metric is realized by the expected explicit map.

N1–N2 — the theorem applies to concrete metrics

noncomputable def NashTorusWitnessTests.bumpyMetric (n : ℕ) (hn : 0 < n) : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ

An $x$-dependent conformally flat metric (2 + sin x₀) · I.

Equations

• NashTorusWitnessTests.bumpyMetric n hn x = (2 + Real.sin (x ⟨0, hn⟩)) • 1

theorem NashTorusWitnessTests.bumpyMetric_pos {n : ℕ} (hn : 0 < n) (x : Fin n → ℝ) : 0 < 2 + Real.sin (x ⟨0, hn⟩)

theorem NashTorusWitnessTests.bumpyMetric_isPosDefSmoothMetric {n : ℕ} (hn : 0 < n) : NashEmbedding.IsPosDefSmoothMetric (bumpyMetric n hn)

N3 — Realizes is not vacuous

N4 — IsInjectiveEmbedding is not vacuous

N5 — the injectivity lattice is 2πℤⁿ

noncomputable def NashTorusWitnessTests.doubledCircle : (Fin 1 → ℝ) → Fin 2 → ℝ

The doubled circle map x ↦ (cos 2x₀, sin 2x₀) on ℝ¹.

Equations

• NashTorusWitnessTests.doubledCircle x = ![Real.cos (2 * x 0), Real.sin (2 * x 0)]

N6 — the expected explicit realization