# Verified Physics

Machine-verified numerical kernels for physical simulations.

## Black Hole Mechanics

Schwarzschild and Kerr black hole thermodynamics verified with Lean 4 + Fortran + Coq.
Every numerical result is within 1 ULP of the exact formula.

```bash
cd bh-mechanics && make test
# 14/14 tests pass, all ULP-verified
```

### What is verified

| Formula | Verification |
|---------|-------------|
| κ = 1/(4M) (Schwarzschild surface gravity) | Fortran + runtime check |
| S = 4πM² (Hawking entropy) | Fortran + runtime check |
| First law: dM = (κ/2π)dS | Fortran |
| Kerr κ, S, Ω exact formulas | Fortran + runtime check |
| LQG correction S = A/4 + α ln A + β | Fortran + runtime check |
| String correction S = A/4 + γ√A | Fortran + runtime check |

### Connection to the Constraint DSL

The entropy bound H ≤ 0.20 nats in the HyperKitty Constraint DSL is an
information-theoretic threshold. The K3 surface (Hodge entropy = 0.831 nats)
violates it. Black hole entropy is a physical analogue of the same principle:
entropy bounds determine what states are thermodynamically admissible.

The BH mechanics kernel applies the same verification methodology to physical
systems: formal specification → numerical implementation → proof that
implementation matches specification within machine precision.

See: [hyperkitty-constraint-dsl](https://github.com/SNAPKITTYWEST/hyperkitty-constraint-dsl)