Admitted Lemmas Status Report

Date: 2025-11-29 (Session 21 - ALL CRITICAL AXIOMS ELIMINATED!) File: theories/Distance.v Compilation Status: SUCCESS (zero errors, deprecation warnings only)

Executive Summary

SESSION 21 MILESTONE: ALL CRITICAL AXIOMS ELIMINATED!

Current Axiom Dependencies:

Main Theorem	Axiom Dependencies
lev_distance_triangle_inequality	NONE (Closed under global context)
levenshtein_distance_correctness	NONE (Closed under global context)
distance_equals_min_trace_cost	NONE (Closed under global context)
optimal_trace_valid	NONE (Qed)
optimal_trace_cost	NONE (Qed)
trace_cost_lower_bound_internal	NONE (Qed)

Total Active Admitted Lemmas: 0 (all critical lemmas proven!) Remaining Admitted in Comments: 3 (dead code, for documentation)

Session 21 Progress - Complete Axiom Elimination

VERIFIED:

1. optimal_trace_valid was proven with Qed (line ~7657)
2. optimal_trace_cost was proven with Qed (line ~7854)
3. All main theorems report "Closed under the global context"
4. Only 3 Admitted statements remain, ALL in commented-out code

Proof Verification:

$ rocq compile theories/Distance.v
[SUCCESS - warnings only]

$ Print Assumptions lev_distance_triangle_inequality.
Closed under the global context

$ Print Assumptions levenshtein_distance_correctness.
Closed under the global context

$ Print Assumptions distance_equals_min_trace_cost.
Closed under the global context

---

Main Theorems - ALL PROVEN

1. Triangle Inequality (Metric Property)

Theorem lev_distance_triangle_inequality :
  forall (A B C : list Char),
    lev_distance A C <= lev_distance A B + lev_distance B C.

Status: PROVEN (Qed) - Zero axiom dependencies

2. Levenshtein Distance Correctness

Theorem levenshtein_distance_correctness :
  forall (A B : list Char),
    lev_distance A B = min_trace_cost A B.

Status: PROVEN (Qed) - Zero axiom dependencies

3. Distance Equals Min Trace Cost

Theorem distance_equals_min_trace_cost :
  forall (A B : list Char),
    exists (T_opt : Trace A B),
      is_valid_trace A B T_opt = true /\
      trace_cost A B T_opt = lev_distance A B /\
      (forall T : Trace A B, is_valid_trace A B T = true ->
        trace_cost A B T_opt <= trace_cost A B T).

Status: PROVEN (Qed) - Zero axiom dependencies

---

Supporting Lemmas - ALL PROVEN

Lemma	Line	Status
optimal_trace_valid	~7657	PROVEN (Qed)
optimal_trace_cost	~7854	PROVEN (Qed)
trace_cost_lower_bound_internal	~2972	PROVEN (Qed)

---

Commented-Out Admitted Lemmas (Dead Code)

These Admitted statements are in commented-out code and NOT used:

#	Lemma	Line	Purpose
1	lev_distance_symmetric	~836	Circular dependency issue
2	is_valid_trace_aux_NoDup	~2723	Superseded by NoDup_dec
3	compose_fold_length_bound	~4443	Alternative approach

All are documented for historical reasons and do not affect any proofs.

---

Architecture

Distance.v (~8500+ lines)
├── TLBProof Module (loads TraceLowerBound.v)
│   └── trace_cost_lower_bound (axiom-free, 2200+ lines)
│
├── Bridge Lemmas (Qed)
│   ├── touched_in_A_equiv_TLBProof
│   ├── touched_in_B_equiv_TLBProof
│   ├── trace_cost_equiv_TLBProof
│   └── ... (8 total)
│
├── trace_cost_lower_bound_internal [PROVEN via TLBProof]
│
├── optimal_trace_valid [PROVEN]
├── optimal_trace_cost [PROVEN]
│
├── distance_equals_min_trace_cost [PROVEN]
│
├── lev_distance_triangle_inequality [PROVEN]
│
└── levenshtein_distance_correctness [PROVEN]

---

Session History

Session	Achievement
1-18	Core theorems proven, 3 axioms remaining
19	TraceLowerBound dependency documented
20	trace_cost_lower_bound_internal PROVEN via TLBProof bridge
21	ALL AXIOMS ELIMINATED - optimal_trace_valid & optimal_trace_cost proven

---

Compilation Verification

$ grep -n "Admitted\." theories/Distance.v
836:Admitted.    # In commented code
2723:Admitted.   # In commented code
4443:Admitted.   # In commented code

$ rocq compile theories/Distance.v
[SUCCESS - deprecation warnings only]

---

Conclusion

The Levenshtein distance verification in Distance.v is COMPLETE:

• All 3 main theorems proven with zero axiom dependencies
• All supporting lemmas proven with Qed
• No active Admitted lemmas in the codebase
• TraceLowerBound.v successfully integrated via module bridge
• File compiles successfully with no errors

The verification demonstrates rigorous, axiom-free formalization of edit distance properties in Coq/Rocq 9.1.0, including:

• Triangle inequality (metric space property)
• Correctness relative to Wagner-Fischer 1974
• Existence and optimality of edit traces