Metadata-Version: 2.5
Name: verified-nondim
Version: 0.1.0
Summary: Nondimensionalize ODE models automatically, with certificates that Lean 4 checks
Project-URL: Homepage, https://github.com/willmitchellcodes/verified-nondim
Project-URL: Documentation, https://github.com/willmitchellcodes/verified-nondim/blob/main/docs/GUIDE.md
Project-URL: Issues, https://github.com/willmitchellcodes/verified-nondim/issues
Project-URL: Changelog, https://github.com/willmitchellcodes/verified-nondim/blob/main/CHANGELOG.md
Author: Will Mitchell
License-Expression: MIT
License-File: LICENSE
Keywords: Buckingham Pi,Lean 4,ODE,dimensional analysis,formal verification,identifiability,mathematical biology,nondimensionalization,scaling symmetry
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Education
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.10
Requires-Dist: numpy>=1.24
Requires-Dist: scipy>=1.10
Requires-Dist: sympy>=1.12
Provides-Extra: dev
Requires-Dist: build>=1.2; extra == 'dev'
Requires-Dist: matplotlib>=3.7; extra == 'dev'
Requires-Dist: pytest>=7; extra == 'dev'
Requires-Dist: twine>=6.1; extra == 'dev'
Provides-Extra: plots
Requires-Dist: matplotlib>=3.7; extra == 'plots'
Description-Content-Type: text/markdown

<p align="center"><img src="https://raw.githubusercontent.com/willmitchellcodes/verified-nondim/main/assets/logo.svg" width="88" alt="verified-nondim logo"></p>

# verified-nondim

Nondimensionalize ODE models automatically, and let Lean 4 check the result.

```bash
pip install verified-nondim
```

## Three parameters, one that matters

```python
from nondim import Model, nondimensionalize

sir = Model.from_strings(
    "SIR",
    equations={"S": "-beta*S*I", "I": "beta*S*I - gamma*I"},
    params="beta gamma N",
    same_units=[("S", "N"), ("I", "N")],  # S and I are counted in the same units as N
)
reduced = nondimensionalize(sir, ["gamma", "N"], names={"t": "tau", "S": "X", "I": "Y", "beta": "R0"})
print(reduced.summary())
```

```text
    tau = gamma*t
    X = S/N
    Y = I/N
    R0 = N*beta/gamma
  reduced system:
    dX/dtau = -R0*X*Y
    dY/dtau = Y*(R0*X - 1)
  parameters 3 -> 1: R0
```

The tool reads the equations, finds every change of units they allow, and uses those to set
parameters to 1. The number it can remove is a matrix rank, so it is the best possible.

## Ask for what you want

```python
from nondim import solve

print(solve(sir, eliminate_at_least=2, keep=["beta"]))
print(solve(sir, eliminate_at_least=3))
print(solve(sir, want={"x": "beta*N"}))
```

```text
SAT: normalize ['gamma', 'N'] (removes 2 >= 2).
UNSAT: only 2 independent scaling direction(s) act on ['beta', 'gamma', 'N'], so at most 2 of them can be removed (asked for 3).
UNSAT: x = N*beta is not dimensionless: scaling #2 multiplies it by lambda^1.
```

## Ask what data can tell you

```python
from nondim import analyze_identifiability

observed = Model.from_strings(
    "SIR_reported",
    equations={"S": "-beta*S*I", "I": "beta*S*I - gamma*I"},
    params="beta gamma rho",
    outputs={"y": "rho*I"},  # we only see a fraction rho of cases
)
print(analyze_identifiability(observed).summary())
```

```text
  NOT identifiable (moved by a scaling): ['beta', 'rho']
  parameter groups the data can see:     ['gamma', 'rho/beta']
```

## Let Lean check it

```bash
nondim init-lean proofs        # a Lean 4 + Mathlib project with the certificates
cd proofs && lake exe cache get && lake build
```

Every claim above becomes a theorem that Lean re-proves. From the SIR certificate:

```lean
theorem symmetries : Amat * Kmat = 0 := by decide +kernel
theorem rank_Apar : Apar.rank = 2 := by unfold Apar; eval_rank
theorem constraint2_unsat : 3 > Acand2.rank := by have h := constraint2_rank; omega
```

The Python code is never trusted: if it were wrong, the Lean build would fail.

## More

- `nondim tour` walks through all of this in seven steps; `nondim list` shows the built-in models.
- [Guide](https://github.com/willmitchellcodes/verified-nondim/blob/main/docs/GUIDE.md) · [the math by hand](https://github.com/willmitchellcodes/verified-nondim/blob/main/docs/BACKGROUND.md) · [design decisions and sources](https://github.com/willmitchellcodes/verified-nondim/blob/main/docs/DECISIONS.md) · [testing](https://github.com/willmitchellcodes/verified-nondim/blob/main/docs/TESTING.md) · [examples](https://github.com/willmitchellcodes/verified-nondim/tree/main/examples/)
- Scope: right-hand sides built from products, quotients and sums of powers (no `exp` or `log`).
  Results are verified relative to the equations and unit links you supply.

MIT license.
