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
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 O2Label
lean-sorry,mathlib-gap,autophagy