Saved in:
| Main Author: | |
|---|---|
| Format: | Recurso digital |
| Language: | |
| Published: |
Zenodo
2026
|
| Subjects: | |
| Online Access: | https://doi.org/10.5281/zenodo.20008839 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866902025240838144 |
|---|---|
| author | Hart, Justin |
| author_facet | Hart, Justin |
| contents | Machine-verified Lean 4 / Mathlib proofs for the thermodynamic analysis of plasma-mediated atmospheric nitrogen fixation (Hart 2026). 38 theorems, lemmas, corollaries, and system invariants. Zero sorry statements. Axioms: propext, Classical.choice, Quot.sound. Part of the Viridis Applied Proofs Series, supplementing the Intelligence Bound foundational canon (DOI: 10.5281/zenodo.20006414). Formal verification performed by Aristotle (Harmonic), project ID 7fc5f57e-1abb-4126-80fd-86daf035063e. Notable finding: verification uncovered a minor unit-conversion inconsistency in Theorem 4 (T4) of the paper, with all downstream arithmetic internally consistent. |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_20008839 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Formal Verification of Plasma-Mediated N₂ Fixation — Viridis Applied Proofs Series 1 Hart, Justin formal verification Lean 4 Mathlib Aristotle Harmonic plasma chemistry nitrogen fixation thermodynamics Haber-Bosch alternative energy efficiency atmospheric N2 Viridis canon machine-checked proof P7 module sustainable agriculture green chemistry Machine-verified Lean 4 / Mathlib proofs for the thermodynamic analysis of plasma-mediated atmospheric nitrogen fixation (Hart 2026). 38 theorems, lemmas, corollaries, and system invariants. Zero sorry statements. Axioms: propext, Classical.choice, Quot.sound. Part of the Viridis Applied Proofs Series, supplementing the Intelligence Bound foundational canon (DOI: 10.5281/zenodo.20006414). Formal verification performed by Aristotle (Harmonic), project ID 7fc5f57e-1abb-4126-80fd-86daf035063e. Notable finding: verification uncovered a minor unit-conversion inconsistency in Theorem 4 (T4) of the paper, with all downstream arithmetic internally consistent. |
| title | Formal Verification of Plasma-Mediated N₂ Fixation — Viridis Applied Proofs Series 1 |
| topic | formal verification Lean 4 Mathlib Aristotle Harmonic plasma chemistry nitrogen fixation thermodynamics Haber-Bosch alternative energy efficiency atmospheric N2 Viridis canon machine-checked proof P7 module sustainable agriculture green chemistry |
| url | https://doi.org/10.5281/zenodo.20008839 |