Repository navigation

feat(Analysis/ODE/Caratheodory): formalize Carathéodory existence, uniqueness, and state-space realization graphs - #69

Open

AdoHaha wants to merge 7 commits into

mcdoll:mainfrom

AdoHaha:feat/caratheodory

Open

feat(Analysis/ODE/Caratheodory): formalize Carathéodory existence, uniqueness, and state-space realization graphs#69
AdoHaha wants to merge 7 commits into
mcdoll:mainfrom
AdoHaha:feat/caratheodory

Commits on Sep 7, 2026
- feat(Analysis/ODE/GlobalExistence): prove unique, add_apply, and add_apply''
  Igor
  committed
  796914b
- feat(InputOutput): prove isGraph_inputOutput and isGraph_inputState
  Igor
  committed
  dae4c72
- feat(ODE): prove linear_fundamental_solution and linear_fundamental_solution'
  Igor
  committed
  336ee32
- feat(Dynamics): prove isCompleteVectorField for IsLinearlyBddVectorField
  Igor
  committed
  87e7e02
Commits on Sep 12, 2026
- feat(Analysis/ODE/Caratheodory): formalize Caratheodory ODE existence, uniqueness, and state-space realizations
  Igor
  committed
  5a2c8fe
Commits on Sep 30, 2026
- Merge upstream main into Caratheodory branch
  Igor
  committed
  dc97e88
- Keep closed-loop graph proofs scoped to PR 71
  Igor
  committed
  ccb4966