CavityPrecisionPath.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The affine precision homotopy in cav:q-precision. Since the eigenvectors of its fixed symmetric coefficient do not change, path nonsingularity rules out eigenvalues at or above one directly.

lemma OAI.InvariantIsing.cavity_precision_eigenvalues_lt_one line 15
lemma OAI.InvariantIsing.cavity_precision_inner_pos line 39
theorem OAI.InvariantIsing.cavity_precision_posDef_of_path line 73
Source documentation
The source's precision-continuation argument specialized to its actual affine path. No continuity-of-eigenvalues input is needed.
```
theorem cavity_precision_posDef_of_path {d : ℕ}
    (M : Matrix (Fin d) (Fin d) ℝ) (hM : M.IsHermitian)
    (hpath : ∀ t ∈ Set.Icc (0 : ℝ) 1, IsUnit (1 - t • M).det) :
    (1 - M).PosDef := by
…
```