{"fqn":"KLean.Bio.TMScoreNonneg.tmScore_nonneg","short":"tmScore_nonneg","module":"KLean.Bio.TMScoreNonneg","path":"KLean/Bio/TMScoreNonneg.lean","claim":"The TM-score, an average of terms 1/(1+(d/d0)^2) over the target length, is nonnegative when all residue distances are nonnegative.","verified":true,"axiom_level":"kernel-standard","olean_sha256":"8a92fe73b9fc3a162472ce0928e7fc43bac3ca8f5e04a275f253426a35fde67b","quarantined":false,"statement":"theorem tmScore_nonneg (d_i : ℕ → ℝ) (L_target : ℕ) (d0 : ℝ) (hL : 0 < L_target) (hd0 : 0 < d0) (hd_nonneg : ∀ i, 0 ≤ d_i i) : 0 ≤ tmScore d_i L_target d0 hL hd0","topics":["biology"],"refs":["https://doi.org/10.1002/prot.20264"],"depends_on":["KLean.Misc.Basic"],"used_by":[],"compute":"/api/v1/klean/compute/tm_score","seal":{"receipt_id":"d017cc7dffff572a7adc3c1d","digest":"ff9469cecfb2bfdf74174682d2499bf3dcc86c0d62e7197d6640fab11f61bd22","sealed_at":"2026-08-10T03:30:24.740384+00:00","time_source":"roughtime_chain"},"commit":"4b8413e1b8"}