| ← Back to Home | Research | Publications |
Principal Investigator Award Application — Harmonic Aristotle AI Grants
| PI: César A. Vargas García, PhD | Principal Investigator, AGROSAVIA (Colombia) |
| Requested Funding: $100,000 | Duration: 24 months |
We propose to advance the formal verification of Stochastic Hybrid Systems (SHS) theory in Lean 4, extending our existing formalization to three domains: (1) complete cell size control theory including exponential growth, multi-step division, and changing environments, (2) gene expression dynamics, and (3) theoretical systems agriculture (stochastic crop modeling). This two-year project bridges rigorous mathematical foundations with practical applications for biology and smallholder farmers.
Our team has completed a production-grade Lean 4 formalization of SHS theory based on Hespanha’s foundational framework (2005), released as SHSLib (project details). The following core results are fully verified (2,500+ lines, Lean 4.24.0 with Mathlib):
The complete SHS 6-tuple $(n, Q, m, f, \phi, \lambda)$:
Dynkin’s Formula (Theorem 1): $\mathbb{E}[\psi(\mathbf{z}(t))] = \psi(z_0) + \mathbb{E}\left[\int_{t_0}^t (\mathcal{L}\psi)(\mathbf{z}(s))\, ds\right]$
For cells with linear growth $\mu$ and division rate $k$:
\[\frac{dM_1}{dt} = \mu - \frac{k}{2}M_1 \quad \Rightarrow \quad \mathbb{E}[X^*] = \frac{2\mu}{k}\]| Result | Formula | Status |
|---|---|---|
| Variance | $\text{Var}[X] = \frac{4}{3}(\mu/k)^2$ | Verified |
| CV | $1/\sqrt{3} \approx 0.577$ | Verified |
| Skewness | $6\sqrt{3}/7 \approx 1.485$ | Verified |
| Characteristic function | $C(\xi) = \prod_{j=0}^{\infty} (1-i(\mu/k)2^{-j}\xi)^{-1}$ | Verified |
| Density series | $\rho^*(x) = \sum_{n=0}^{\infty} c_n e^{-(k/\mu)2^n x}$ | Verified |
| Upwind scheme stability | CFL condition verified | Verified |
| MLE for division rate | $\hat{k} = N/T$ maximizes likelihood | Verified |
This proposal builds on 15+ years of research in stochastic cell size control:
Scientific Reports (2016): A mechanistic stochastic framework for regulating bacterial cell division — Established first-passage time models reproducing the “adder principle” and scale-invariant size distributions. This paper’s mathematical framework is the foundation of our Lean 4 formalization.
Current Biology (2023): A cell-based model for size control in Chlamydomonas reinhardtii — Extended stochastic models to multiple fission organisms with multi-step division cycles. Analysis of ~1,900 cells validated the Modified Threshold model.
arXiv (2025): Dynamical Inference of Cell Size Regulation Parameters — Parameter estimation under changing growth conditions, directly relevant to proposed formalization extensions.
Building on our verified linear model, we will formalize:
A. Exponential Growth Dynamics
Most cells grow exponentially ($\dot{x} = \mu x$), not linearly. We will formalize:
B. Multi-Step Division Process
Cells often require multiple molecular steps before division (e.g., DNA replication checkpoints). We will formalize:
C. Changing Growth Conditions
Real cells experience nutrient shifts. We will formalize:
D. Multi-Dimensional Correlations
Using our 4D cell tracking SHS $(x, \tau, x_b, x_d)$:
Establish formally verified crop modeling extending DSSAT/APSIM:
| Category | Amount | Purpose |
|---|---|---|
| Graduate Students | $50,000 | Two MS/PhD students for formalization (24 months, 50% FTE) |
| Professional Developer | $30,000 | Lean 4 expert for library architecture (12 months, 50% FTE) |
| Computational Resources | $10,000 | Cloud computing, CI/CD infrastructure |
| Software & Dissemination | $10,000 | Smallholder tools, open-source release, workshops |
| Period | Milestone |
|---|---|
| Q1-Q2 | Exponential growth formalization; multi-step division SHS |
| Q3-Q4 | Changing conditions dynamics; 4D correlation derivations |
| Q5-Q6 | Gene expression bursting; noise decomposition proofs |
| Q7-Q8 | Crop growth SHS; yield distribution theory; library release |
Final Outputs:
Our 2,500+ lines of verified Lean 4 demonstrate feasibility. Aristotle will accelerate:
Our unique position—deep theoretical expertise in cell size control plus agricultural applications—ensures impact beyond pure mathematics.
| Contact: cavargas@agrosavia.co | ORCID | Google Scholar |
Supporting Harmonic’s mission to democratize rigorous mathematical reasoning while addressing challenges in food security and human health.
| ← Back to Home | Research | Publications |