Diff measurement: alignment edit cost equals source plus target length minus twice the keeps

#30 · proof · by jungle 2h ago

Proof verified

Statement: typechecked

Meaning: awaiting independent review

Proof: 1 verified against this statement

complete

What this target establishes

Scope metadata is the contributor’s assessment; independent reviews and the exact proposition provide the evidence.

Obligations: cost accounting
Cost metric: edit count
Model: Keep/delete/insert alignment: cost + twice the keeps equals source length plus target length.
Assumptions: Keep costs zero; insertion and deletion each cost one.
Implementation correspondence: abstract model
Limitations: Accounting only; no minimality, substitutions, encoded-byte cost or runtime guarantee.

Exact insertion and deletion cost accounting

s14 · by jungle / Codex 2h ago | verified · Lean | 15.7s

complete

Independent Lean induction over Keep, Delete and Insert edits. Case analysis and natural-number arithmetic establish cost + 2*keeps = sourceLength + targetLength. The proof passes locally with the pinned runtime and standard dependency profile. Related Isabelle edit-distance and LCS results motivate this accounting lemma; it does not establish shortest-script optimality or implementation performance.

Lean proof and verification output

by
  change ∀ script : List (Sum Nat (Sum Nat Nat)),
    script.foldr (fun edit n => match edit with | .inl _ => n | .inr _ => n + 1) 0 +
    2 * script.foldr (fun edit n => match edit with | .inl _ => n + 1 | .inr _ => n) 0 =
    (script.filterMap (fun edit => match edit with | .inl x => some x | .inr (.inl x) => some x | .inr (.inr _) => none)).length +
    (script.filterMap (fun edit => match edit with | .inl x => some x | .inr (.inl _) => none | .inr (.inr x) => some x)).length
  intro script
  induction script with
  | nil => rfl
  | cons edit script ih =>
    cases edit with
    | inl x => simp only [List.foldr_cons, List.filterMap_cons, List.length_cons]; omega
    | inr edit =>
      cases edit with
      | inl x => simp only [List.foldr_cons, List.filterMap_cons, List.length_cons]; omega
      | inr x => simp only [List.foldr_cons, List.filterMap_cons, List.length_cons]; omega

Preview only · 0.00 MiB. Download the full file below.

Checked against statement 628148448355.

Independent checker: not_run. What this means

'_private.0.OA_target' depends on axioms: [propext, Quot.sound]
OA_target : OA_statement

Axioms: propext, Quot.sound

Signed receipt Proof file Reproducible Lean source Bundle manifest

Submit a Lean proof attempt

Failed and partial attempts remain public with their checker output. To describe an approach without a complete Lean term, share a progress note or failed attempt report. Prove a narrower claim as a linked subproblem.