v1.0.4

Strengthen the formal result to show that p -> p is not a substitution instance of any member of the condensed-detachment closure. Add and verify substitution-weight monotonicity, replace three incidental native_decide base cases with kernel-checked proofs, align theorem comments with the JAR sequel manuscript, and correct the README.

v1.0.3

Add TPTP input and Python verification script; update paper title

Consolidate to single proof file

Simplified project structure: all definitions and proofs now in a single U4Lean.lean file (440 lines). No changes to the proof itself.

v1.0.1: Formal verification that u4 is not a single axiom

Lean 4 formal verification (zero sorry, no Mathlib dependency) that Ulrich's candidate u4 is not a single axiom for positive implication.

Main result: thm5_not_unifiable — For all i ≥ 1, j ≥ 0, CD(T_i, T_j) is undefined.

Corollary: p → p is not derivable from u4, so Meredith's 17-symbol axiom is the shortest single axiom for positive implication.

Requires Lean 4.28.0-rc1. Build with lake build.

v1.0.0: Formal verification that u4 is not a single axiom

Lean 4 formal verification (zero sorry, no Mathlib dependency) that Ulrich's candidate u4 is not a single axiom for positive implication.

Main result: thm5_not_unifiable — For all i ≥ 1, j ≥ 0, CD(T_i, T_j) is undefined.

Corollary: p → p is not derivable from u4, so Meredith's 17-symbol axiom is the shortest single axiom for positive implication.

Requires Lean 4.28.0-rc1. Build with lake build.