chore(proofs): add TPTP corpus + known-good Agda witness

proofs/tptp/*.p — 8 hand-written first-order problems:
  modus_ponens, transitivity, socrates, group_left_identity,
  contradiction, disjunction_elim, double_negation, symmetry_eq

Small, clean FOF problems for exercising Vampire / E Prover / SPASS
runners. All but contradiction.p are Theorems; contradiction.p is
deliberately CounterSatisfiable so the runner's unknown-outcome
branch gets exercised.

proofs/agda/IdentityLaws.agda — trivial proofs of +-left-id and
+-right-id over ℕ, compiles cleanly against agda-stdlib v2.3.
Serves as a known-good witness alongside the pre-existing Agda files
which have their own scope/precedence bugs.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/agda/IdentityLaws.agda

@@ -0,0 +1,18 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- IdentityLaws.agda — trivial proofs that compile cleanly against
+-- agda-stdlib v2.3. Exists to exercise the echidnabot agda runner
+-- with a known-good file alongside the pre-existing (broken) corpus.
+
+module IdentityLaws where
+
+open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+
+-- Addition has zero as left identity, by definition.
++-left-id : (n : ℕ) → zero + n ≡ n
++-left-id _ = refl
+
+-- Zero as right identity needs induction on n.
++-right-id : (n : ℕ) → n + zero ≡ n
++-right-id zero    = refl
++-right-id (suc n) = cong suc (+-right-id n)

proofs/tptp/contradiction.p

@@ -0,0 +1,12 @@
+%-----------------------------------------------------------------------------
+% SPDX-License-Identifier: PMPL-1.0-or-later
+% File     : contradiction.p
+% Status   : CounterSatisfiable
+% Claim    : Deliberately unprovable: asserting P and ¬P.
+%            ATPs should report CounterSatisfiable (or Unsatisfiable of the
+%            axioms, depending on mode) — any answer other than "Theorem"
+%            is correct.
+%-----------------------------------------------------------------------------
+fof(p,     axiom, p).
+fof(not_p, axiom, ~ p).
+fof(goal,  conjecture, q).

proofs/tptp/disjunction_elim.p

@@ -0,0 +1,10 @@
+%-----------------------------------------------------------------------------
+% SPDX-License-Identifier: PMPL-1.0-or-later
+% File     : disjunction_elim.p
+% Status   : Theorem
+% Claim    : Disjunction elimination — from P∨Q, P→R, Q→R, conclude R.
+%-----------------------------------------------------------------------------
+fof(p_or_q, axiom, p | q).
+fof(p_imp,  axiom, p => r).
+fof(q_imp,  axiom, q => r).
+fof(goal,   conjecture, r).

proofs/tptp/double_negation.p

@@ -0,0 +1,8 @@
+%-----------------------------------------------------------------------------
+% SPDX-License-Identifier: PMPL-1.0-or-later
+% File     : double_negation.p
+% Status   : Theorem
+% Claim    : ¬¬P → P (classical double-negation elimination).
+%-----------------------------------------------------------------------------
+fof(not_not_p, axiom, ~ ~ p).
+fof(goal,      conjecture, p).

proofs/tptp/group_left_identity.p

@@ -0,0 +1,12 @@
+%-----------------------------------------------------------------------------
+% SPDX-License-Identifier: PMPL-1.0-or-later
+% File     : group_left_identity.p
+% Status   : Theorem
+% Claim    : In a group, e is also a right identity (proved from left-identity
+%            + left-inverse axioms — a classical group-theory exercise).
+%-----------------------------------------------------------------------------
+fof(left_id,      axiom, ! [X] : mult(e, X) = X).
+fof(left_inv,     axiom, ! [X] : mult(inv(X), X) = e).
+fof(assoc,        axiom,
+    ! [X,Y,Z] : mult(X, mult(Y, Z)) = mult(mult(X, Y), Z) ).
+fof(right_id_goal, conjecture, ! [X] : mult(X, e) = X).

proofs/tptp/modus_ponens.p

@@ -0,0 +1,10 @@
+%-----------------------------------------------------------------------------
+% SPDX-License-Identifier: PMPL-1.0-or-later
+% File     : modus_ponens.p
+% Syntax   : TPTP FOF (First-Order Form)
+% Status   : Theorem
+% Claim    : Modus ponens: from P and P→Q, conclude Q.
+%-----------------------------------------------------------------------------
+fof(p,        axiom,    p).
+fof(p_imp_q,  axiom,    p => q).
+fof(goal,     conjecture, q).

proofs/tptp/socrates.p

@@ -0,0 +1,11 @@
+%-----------------------------------------------------------------------------
+% SPDX-License-Identifier: PMPL-1.0-or-later
+% File     : socrates.p
+% Status   : Theorem
+% Claim    : Classical syllogism: all humans are mortal; Socrates is human;
+%            therefore Socrates is mortal.
+%-----------------------------------------------------------------------------
+fof(all_humans_mortal, axiom,
+    ! [X] : (human(X) => mortal(X)) ).
+fof(socrates_is_human, axiom, human(socrates)).
+fof(goal, conjecture, mortal(socrates)).

proofs/tptp/symmetry_eq.p

@@ -0,0 +1,8 @@
+%-----------------------------------------------------------------------------
+% SPDX-License-Identifier: PMPL-1.0-or-later
+% File     : symmetry_eq.p
+% Status   : Theorem
+% Claim    : Equality is symmetric: a=b → b=a (follows from equality axioms).
+%-----------------------------------------------------------------------------
+fof(h, axiom, a = b).
+fof(goal, conjecture, b = a).

proofs/tptp/transitivity.p

@@ -0,0 +1,11 @@
+%-----------------------------------------------------------------------------
+% SPDX-License-Identifier: PMPL-1.0-or-later
+% File     : transitivity.p
+% Status   : Theorem
+% Claim    : Less-than is transitive: a<b ∧ b<c → a<c.
+%-----------------------------------------------------------------------------
+fof(trans, axiom,
+    ! [X,Y,Z] : (lt(X,Y) & lt(Y,Z) => lt(X,Z)) ).
+fof(h1, axiom, lt(a,b)).
+fof(h2, axiom, lt(b,c)).
+fof(goal, conjecture, lt(a,c)).