O1: separation_theorem — eigenvalue API gap (Mathlib.LinearAlgebra.Matrix.Spectrum)

[TOTOGT]

Status

Open — 1 scoped sorry in PrincipiaVol1.lean §9

What is proved

• The bound structure: |Tr(M) − 1| < 1 implies Tr(M) ≠ 33
• The arithmetic: exp(−12) < 1/32
• The bound on n: n − 1 ≤ 32 for n < 33

What the sorry guards

The step from IsDm3Stable M (diagonal bound predicate) to the
sum bound |Tr(M) − 1| < 1 requires accessing individual eigenvalues
from the diagonal of a real matrix with bounded spectral radius.

This requires Mathlib.LinearAlgebra.Matrix.Spectrum applied to
diagonal entries — not yet in stable Mathlib4 in the form needed.

Closure path

[TOTOGT]

Issue #12 :

Title:

O1: separation_theorem — eigenvalue API gap (Mathlib.LinearAlgebra.Matrix.Spectrum)

Body:

## Status
Open — 1 scoped sorry in `PrincipiaVol1.lean §9`

## What is proved
- The bound structure: `|Tr(M) − 1| < 1` implies `Tr(M) ≠ 33`
- The arithmetic: `exp(−12) < 1/32`
- The bound on n: `n − 1 ≤ 32` for `n < 33`

## What the sorry guards
The step from `IsDm3Stable M` (diagonal bound predicate) to the
sum bound `|Tr(M) − 1| < 1` requires accessing individual eigenvalues
from the diagonal of a real matrix with bounded spectral radius.

This requires `Mathlib.LinearAlgebra.Matrix.Spectrum` applied to
diagonal entries — not yet in stable Mathlib4 in the form needed.

## Closure path

Mathlib.LinearAlgebra.Matrix.Spectrum

• Finset.sum bound on |M i i ^ 6|
• Real.exp_neg_two_le_one for the transverse bound

## Referenced in
- `PrincipiaVol1.lean` §9, `separation_theorem`
- `OPEN_QUESTIONS.md` row O1
- `principia_vol1_v2_full.pdf` §17
- `principia_vol1.html` §17

## Label
`lean-sorry`, `mathlib-gap`, `vol1`

---

Issue #14 — already referenced, may exist. If not:

Title:

O2: AutophagyDm3 — Mather C∞-stability (Ob.2) and Poincaré–Bendixson (Ob.3)

Body:

## Ob.2 — whitneyFold_conditional
Sorry guards Mather's C∞-stability theorem.
Algebraic content proved: V_factored, V_critical_at_one, V_second_deriv_ne_zero.
Antecedent (mTORC1 suppression map is Morse near ρ*) requires kinase data.
Closure path: Mather stability once in Mathlib + biology data.

## Ob.3 — limitCycle_exists_auto
Compactness content proved: dm3_basin_compact, dm3_basin_nonempty.
Sorry guards only the Poincaré–Bendixson conclusion.
Closure path: Mathlib.Dynamics.OmegaLimit + PB infrastructure.

## Files
`AutophagyDm3_v2.lean`, `PrincipiaVol1.lean §13 O2`

## Label
`lean-sorry`, `mathlib-gap`, `autophagy`

---

Issue #15 — already referenced:

Title:

O3: Theorem T1 — full ODE Gronwall integration (z(t) monotonicity)

Body:

## Partial closure (V3)
`gronwall_contraction_below_stability_radius` in `PrincipiaVol1.lean §8`
proves the decay exponent sign: (μmax + 3ε)·T* < 0 for all ε < 1/3.
This is 0 sorry. This is the necessary condition for contraction.

## What remains open
The full bound: ‖δxₜ‖ ≤ ‖δx₀‖·exp((μmax + 3ε)·t)
Requires defining the dm³ vector field as a C¹ map and invoking
`Mathlib.Analysis.ODE.Gronwall` on the explicit ODE.

## Closure path
1. Define dm³ semiflow formally in Lean
2. Prove vector field is C¹ on the Gronwall basin
3. Apply `ODE.Gronwall` to get the exponential bound
4. Conclude z(t) monotonicity from ż = r² − 2(r−1)²e^{−z} ≥ 0

## Files
`PrincipiaVol1.lean §8`, `gronwall_proof.lean`

## Label
`lean-sorry`, `mathlib-gap`, `theorem-T1`

---

After creating all three, add these labels in the Labels tab (create them if they don't exist):

• lean-sorry — red
• mathlib-gap — yellow
• vol1 — blue
• autophagy — green
• theorem-T1 — purple

---