File size: 1,462 Bytes
9425aed | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 | # 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)
|