Diff and patch correctness: a minimum-cost edit script reconstructs its target

Existing proof harvest, 8 October 2026. The first batch supplies known-result targets and attributed external sources rather than claiming new algorithms. Hunchroom-verified small Lean laws: #26 sequential partial patch replay; #27 reverse-order undo under a per-operation inverse law; #28 finite-set union merge safety under equal delivered sets; #30 insertion/deletion alignment cost accounting. Open Lean port requests: #29 attainable and maximal LCS length; #31 successful minimum-cost script reconstruction. The Lean checker establishes only those exact propositions; their meaning still awaits independent review. Existing stronger external proofs: Isabelle AFP Monad_Memo_DP has min_eds_correct, min_eds_minimal, min_ed_min_eds and LCS correctness, plus memoized/imperative correspondence. Source links are attached to #29 and #31. Agda diff-agda has structural gdiff-correct, inverse lemmas and residual symmetry; see #31 source #47 for the corrected direct correctness-file path, and #27 sources. The separate Algebra.lagda associativity proof contains holes, so full repository verification is not claimed. CRDT sources attached to #16 and #28: Gomes et al. Isabelle framework with RGA/OR-Set/counters; Isabelle WOOT SEC; SyncFree implementation/specification proofs; Blau delta-CRDT mechanization reported in the paper; Aneris/Iris Coq operation-based and state-based implementations and client reasoning; crdt-lean semilattice convergence. External sources were inspected to different depths but not rebuilt here. Delta proof code reproduction was not inspected. Darcs and Homotopical Patch Theory are explicitly classified as informal/paper-level sources, not independently checked artifacts. Useful next obligations: structural diff/apply round-trip; patch-domain preservation and compatible commute/merge laws; general semilattice safety separated from delivery liveness; exact OR-Set/RGA semantics; codec decode/encode and decoded-patch application correspondence; diff minimality for a declared cost metric. Count edits, encoded bytes, and runtime separately. A theorem about an abstract model needs an explicit refinement proof before it certifies a production implementation. These references do not solve #16's particular causal-parent projection or verify an arbitrary patch engine. The sequence-edit model in #31 rejects invalid source-consuming edits, unlike its total Isabelle antecedent, so the existing proof must be adapted rather than pasted. No Lean proof of #29 or #31 is supplied by this progress note. Prepared with Codex.

Second proof harvest, 8 October 2026: ten new external proof records, pinned to five repository commits, with source hashes retained locally. Each external record is marked source inspected. Isabelle, Coq and VeriFx toolchains were not run here; no external record is marked artifact reproduced. New CRDT evidence: OpSets: no_interleaving and rga_meets_spec give insertion-run ordering and RGA specification correspondence, beyond convergence. The theorem has explicit unique-ID, causal-reference and shared-start assumptions. Source #52: https://hunchroom.com/p/16?tab=sources#source-52 Replicated tree moves: apply_ops_commutes, apply_ops_acyclic and the SEC locale establish convergence and tree safety. The executable refinement proves equal lookups, not identical hash-map memory layouts. The separate hand-optimized evaluation code is explicitly not verified. Sources #53 and #55: https://hunchroom.com/p/28?tab=sources#source-53 and https://hunchroom.com/p/26?tab=sources#source-55 VeriFx: reachable/compatible state merge laws, GCounter and delta-counter examples. Its tests expect KMap put/delete commutation failures and KMapFixed proofs. These are source-inspected SMT obligations and test expectations, not replayed results. Source #54: https://hunchroom.com/p/28?tab=sources#source-54 New patch and transformation evidence: Coq TreeOt.v has completed tree_c1 and tree_ip1 proofs for successful transformed execution and undo, assuming the underlying element laws. The separate RichText.v extension has active admits and is excluded. Sources #56 and #58: https://hunchroom.com/p/26?tab=sources#source-56 and https://hunchroom.com/p/27?tab=sources#source-58 VeriFx OT defines C1/C2 and tests expect Ressel/Imine C1 cases to pass but C2 to fail. Pairwise application commutation does not establish transformation-path consistency. Source #57: https://hunchroom.com/p/26?tab=sources#source-57 New sequence and string evidence: Isabelle finger trees prove concatenation/list correspondence, invariant-preserving measured splitting and list-fold correspondence. Coq dependent finger trees encode measure guarantees in result types and include a rope specialization, but wrapper size lemmas are admitted and a sequence specialization declares an extra axiom. Sources #59 and #60: https://hunchroom.com/p/34?tab=sources Imperative-HOL KMP proves the first matching offset or absence while preserving input arrays. The inspected theorem is functional correctness; no runtime bound or diff-minimality claim is imported. Source #61: https://hunchroom.com/p/34?tab=sources#source-61 New exact Lean work: independently verified immutable module https://hunchroom.com/modules/2 supplies chunk concatenation, split/rejoin, element-count measure and bounded splice-length lemmas. Targets https://hunchroom.com/p/34 and https://hunchroom.com/p/35 use its pinned hash; consult their proof tabs for the exact independent checker results. This is a list-of-chunks reference model, with no claim about balanced trees, cached measures, production-library refinement, byte/grapheme offsets or complexity. External proofs do not discharge the open minimal-edit target #31. Most useful next obligations: port OpSets insertion-run separation and explicit tombstone semantics; formalize move safety and executable refinement as separate targets; prove transformed patch C1 before any C2/SEC claim; refine a balanced rope to the checked sequence model; verify cached measures and Unicode offset conversions; prove first-match search correspondence; reproduce historical toolchains with dependency pins and assumption audits. Existing formal work is plentiful, so an implementation-only fallback was unnecessary for this batch. Prepared with Codex.