# Derived physics lemmas — proof database v1

[[entry]]
id = "P-LM-ENERGY-001"
kind = "lemma"
field = "physics"
statement = "Kinetic energy T = ½ m v² consistent with scalar speed squared."
proof_status = "proved"
gap_kind = "none"
gap_id = "G-physics"
lean_module = "docs/semantics/Discharge.lean"
lean_thm = "kinetic_energy_def_consistent"
li_specimen = ""
last_verified_lic_commit = "a9542bfc"

[[entry]]
id = "P-LM-MOM-001"
kind = "lemma"
field = "physics"
statement = "Linear momentum p = m v for point mass."
proof_status = "proved"
gap_kind = "none"
gap_id = "G-physics"
lean_module = "docs/semantics/Discharge.lean"
lean_thm = "linear_momentum_linear_stub"
li_specimen = ""
last_verified_lic_commit = "a9542bfc"

[[entry]]
id = "P-LM-CONS-001"
kind = "lemma"
field = "physics"
statement = "Closed-system energy and momentum invariants compose from MECH + CONS axioms (integrator window)."
proof_status = "open"
gap_kind = "modeling_gap"
gap_id = "G-physics"
lean_module = "proof-db/physics/lemmas/energy_drift_bound.li"
lean_thm = ""
li_specimen = "proof-db/physics/lemmas/energy_drift_bound.li"
li_tests = [
  "li-tests/benchmarks/tier0_correctness/md_energy_single_step.li",
  "li-tests/benchmarks/tier0_correctness/three_body_invariants.li",
]
bench_refs = [
  "benchmarks/tier2_physics/md_lennard_jones",
  "benchmarks/tier2_physics/three_body",
]
last_verified_lic_commit = "a9542bfc"
