{"fqn":"KLean.Atoms.Bio.SequenceIdentityNonneg.seqIdentity_nonneg","short":"seqIdentity_nonneg","module":"KLean.Atoms.Bio.SequenceIdentityNonneg","path":"KLean/Atoms/Bio/SequenceIdentityNonneg.lean","claim":"Sequence identity, matches divided by length, is nonnegative for nonnegative matches and positive length.","verified":true,"axiom_level":"kernel-standard","olean_sha256":"bf3ed64e17f47d28fe658cce7712da8339ec86708f5cdce2b9085f81f2bf2f55","quarantined":false,"statement":"theorem seqIdentity_nonneg (numMatches len : ℝ) (hm : 0 ≤ numMatches) (hlen : 0 < len) : 0 ≤ seqIdentity numMatches len","topics":["biology"],"refs":[],"depends_on":["KLean.Atoms.Bio.SequenceIdentityRatio"],"used_by":[],"compute":null,"seal":{"receipt_id":"d017cc7dffff572a7adc3c1d","digest":"ff9469cecfb2bfdf74174682d2499bf3dcc86c0d62e7197d6640fab11f61bd22","sealed_at":"2026-08-10T03:30:24.740384+00:00","time_source":"roughtime_chain"},"commit":"4b8413e1b8"}