ci: blocking statement-fidelity (non-vacuity) gate on changed Lean files

.github/workflows/ci.yml

@@ -78,6 +78,18 @@ jobs:
       - name: Verify witness quality (ban fake check-only witnesses)
         run: bash scripts/check_witness_quality.sh
 
+      # Statement-level non-vacuity: lints the .lean files CHANGED by this PR
+      # for near-vacuity shapes (∀var ∃const quantifier inversion, `: True`
+      # conclusion, `: False` hypothesis) that build/axiom/witness gates miss,
+      # and fails on any unsigned flag. A genuine statement that trips the lint
+      # carries an inline `-- fidelity:` sign-off. Self-tests its detector on a
+      # vacuous/genuine fixture pair. The base ref is passed so the diff is
+      # scoped to the PR; on push it falls back to HEAD~1, else all files.
+      - name: Verify statement fidelity (non-vacuity, changed files)
+        env:
+          FIDELITY_BASE_REF: ${{ github.event.pull_request.base.sha }}
+        run: bash scripts/check_statement_fidelity.sh
+
       - name: Verify no custom constants
         run: |
           if grep -rnE --include="*.lean" '^[[:space:]]*constant[[:space:]]+[^:]+:' FormalSLT/ FormalSLT.lean examples/; then

scripts/check_statement_fidelity.sh

@@ -0,0 +1,128 @@
+#!/usr/bin/env bash
+# Statement-fidelity / non-vacuity gate (BLOCKING).
+#
+# Why this exists: a theorem can build, be axiom-clean, and still be vacuous
+# (e.g. a quantifier-inverted ∀var ∃const bound, a `: True` conclusion, or a
+# `: False` hypothesis). The build/axiom/witness gates do not catch those
+# shapes at the statement level. This gate lints the common near-vacuity shapes
+# on the .lean files touched by a change and FAILS the build on any unsigned
+# flag. A genuinely non-vacuous statement that trips the lint carries an inline
+# `-- fidelity:` sign-off explaining why (e.g. why the constant is uniform);
+# the checker downgrades a signed flag to `ok(signed)`.
+#
+# Scope: it runs on the .lean files CHANGED by the current PR/push (diff vs the
+# base ref), so a clean PR is not blocked by a pre-existing statement elsewhere.
+# When no base ref is resolvable (e.g. a manual run on a detached checkout) it
+# falls back to scanning every tracked .lean file.
+#
+# It then runs a fixture pair to prove the detector discriminates: a synthetic
+# vacuous theorem MUST be flagged (gate would fail), and a synthetic genuine
+# theorem MUST pass. This proves the gate itself works, so a regression that
+# silently neuters the checker is caught.
+#
+# Run from CI alongside the build, axiom, and witness-quality gates.
+set -euo pipefail
+
+ROOT="$(git rev-parse --show-toplevel)"
+cd "$ROOT"
+
+CHECKER="$ROOT/scripts/statement_fidelity_check.py"
+if [ ! -f "$CHECKER" ]; then
+  echo "FAIL: $CHECKER not found" >&2
+  exit 1
+fi
+
+# --- Resolve the set of changed .lean files. ---------------------------------
+# Priority:
+#   1. explicit base ref in FIDELITY_BASE_REF (lets CI pass the PR base sha)
+#   2. GitHub PR base (origin/$GITHUB_BASE_REF) on pull_request events
+#   3. the previous commit (HEAD~1) on a push with history
+#   4. fall back: every tracked .lean file
+base_ref=""
+if [ -n "${FIDELITY_BASE_REF:-}" ] && git rev-parse --verify --quiet "${FIDELITY_BASE_REF}^{commit}" >/dev/null; then
+  base_ref="${FIDELITY_BASE_REF}"
+elif [ -n "${GITHUB_BASE_REF:-}" ]; then
+  git fetch --quiet --depth=1 origin "${GITHUB_BASE_REF}" 2>/dev/null || true
+  if git rev-parse --verify --quiet "origin/${GITHUB_BASE_REF}^{commit}" >/dev/null; then
+    base_ref="origin/${GITHUB_BASE_REF}"
+  fi
+elif git rev-parse --verify --quiet "HEAD~1^{commit}" >/dev/null; then
+  base_ref="HEAD~1"
+fi
+
+declare -a CHANGED=()
+if [ -n "$base_ref" ]; then
+  mb="$(git merge-base "$base_ref" HEAD 2>/dev/null || echo "$base_ref")"
+  echo "== statement-fidelity gate: changed .lean files vs ${base_ref} (merge-base ${mb}) =="
+  while IFS= read -r f; do
+    [ -n "$f" ] || continue
+    case "$f" in *.lean) [ -f "$f" ] && CHANGED+=("$f") ;; esac
+  done < <(git diff --name-only --diff-filter=ACMR "$mb" HEAD)
+else
+  echo "== statement-fidelity gate: no base ref resolvable, scanning all tracked .lean files =="
+  while IFS= read -r f; do
+    [ -n "$f" ] && CHANGED+=("$f")
+  done < <(git ls-files '*.lean')
+fi
+
+fail=0
+
+if [ "${#CHANGED[@]}" -eq 0 ]; then
+  echo "  (no .lean files in scope)"
+else
+  for f in "${CHANGED[@]}"; do
+    out="$(python3 "$CHECKER" "$f" 2>&1)" && rc=0 || rc=$?
+    if [ "$rc" -ne 0 ]; then
+      echo "  FLAG in $f" >&2
+      echo "$out" | sed 's/^/    /' >&2
+      fail=1
+    elif echo "$out" | grep -q 'ok(signed)'; then
+      echo "  ok (signed flag) $f"
+      echo "$out" | grep 'ok(signed)' | sed 's/^/    /'
+    fi
+  done
+  [ "$fail" -eq 0 ] && echo "  ok: ${#CHANGED[@]} changed .lean file(s), no unsigned fidelity flags"
+fi
+
+# --- Fixture pair: prove the detector actually discriminates. -----------------
+echo "== detector fixture pair =="
+WORK="$(mktemp -d)"
+trap 'rm -rf "$WORK"' EXIT
+
+VACUOUS_FIX="$WORK/FixtureVacuous.lean"
+cat > "$VACUOUS_FIX" <<'EOF'
+-- ∀t ∃c, ‖f t‖ ≤ c * g t : the constant is chosen after the variable, so the
+-- bound is trivially satisfiable. The detector MUST flag this (quantifier
+-- inversion). The genuine form is ∃c, ∀t.
+theorem fixture_vacuous {t : ℝ} (f g : ℝ → ℝ) : ∃ c : ℝ, ‖f t‖ ≤ c * (g t) := by
+  sorry
+EOF
+
+GENUINE_FIX="$WORK/FixtureGenuine.lean"
+cat > "$GENUINE_FIX" <<'EOF'
+-- ∃c, ∀t : the constant is uniform over t (quantified inside the ∃). The
+-- detector MUST NOT flag this; it is the genuine, non-vacuous shape.
+theorem fixture_genuine (f g : ℝ → ℝ) : ∃ c : ℝ, ∀ t : ℝ, ‖f t‖ ≤ c * (g t) := by
+  sorry
+EOF
+
+if python3 "$CHECKER" "$VACUOUS_FIX" >/dev/null 2>&1; then
+  echo "  FAIL vacuous fixture was NOT flagged (detector broken)" >&2
+  fail=1
+else
+  echo "  ok   vacuous fixture flagged (detector RED-flags quantifier inversion)"
+fi
+
+if python3 "$CHECKER" "$GENUINE_FIX" >/dev/null 2>&1; then
+  echo "  ok   genuine (∃c ∀t) fixture passed"
+else
+  echo "  FAIL genuine fixture was flagged (detector over-eager)" >&2
+  fail=1
+fi
+
+if [ "$fail" -ne 0 ]; then
+  echo "statement-fidelity gate FAILED" >&2
+  exit 1
+fi
+
+echo "statement-fidelity gate passed: no unsigned fidelity flags, detector verified"

scripts/statement_fidelity_check.py

@@ -0,0 +1,106 @@
+#!/usr/bin/env python3
+"""Statement-fidelity / non-vacuity gate for Lean theorems (NON-NEGOTIABLE).
+
+Vacuity is undecidable in general, so this does the two things that ARE mechanizable and forces the
+rest to an explicit human/adversarial sign-off:
+
+  1. LINT the common near-vacuity shapes (static, regex over theorem statements):
+     - quantifier inversion: a theorem with a free variable param (e.g. {t : ℝ}) whose conclusion is
+       `∃ c ..., ‖f t ...‖ ≤ c * (...)` — i.e. ∀t ∃c, near-vacuous (the constant is chosen AFTER the
+       variable, so the bound is trivially satisfiable). The genuine form is ∃c, ∀t. (This is the
+       INC-2026-06-22 lemma-3 catch.)
+     - trivial conclusion: `: True`, `↔ True`, or a hypothesis that is literally `False`.
+  2. REQUIRE a fidelity sign-off for every load-bearing theorem: a `-- fidelity:` line stating why the
+     statement is non-vacuous (the witness / why the constant is uniform / the adversarial-falsify result),
+     OR the theorem is flagged.
+
+It does NOT replace the adversarial-falsify reasoning pass — it forces it. Run on a Lean file; exit 1 on flags.
+Usage: statement_fidelity_check.py <file.lean> [theorem_name ...]
+"""
+import re, sys
+
+NORM = r'(?:‖|\bnorm\b|abs |\|)'  # a magnitude on the LHS of a bound
+
+def theorems(src):
+    # crude: split on top-level `theorem`/`lemma` keywords, keep name + the statement up to `:= by`/`:=`.
+    # The vacuity lint runs on `stmt` (the statement only). The `-- fidelity:` sign-off, however, may sit
+    # on the comment line(s) immediately ABOVE the keyword or anywhere inside the proof body, so we also
+    # yield a `signoff` window that spans from the preceding comment block through the body up to the next
+    # top-level decl. Without this, a legitimate `-- fidelity:` override never registers (the sign-off line
+    # is outside `stmt`), and the gate would block genuine ∃c-∀var theorems with no working escape hatch.
+    starts = [m.start() for m in re.finditer(r'(?m)^\s*(?:noncomputable\s+)?(?:theorem|lemma)\s+[A-Za-z0-9_\']+', src)]
+    for i, m in enumerate(re.finditer(r'(?m)^\s*(?:noncomputable\s+)?(?:theorem|lemma)\s+([A-Za-z0-9_\']+)', src)):
+        name = m.group(1)
+        start = m.start()
+        nxt = starts[i + 1] if i + 1 < len(starts) else len(src)
+        # bound the body to THIS declaration (next top-level decl, capped) so a statement that ends with
+        # `:= term` (no newline after `:=`) does not bleed into the following theorem and mis-attribute flags.
+        body = src[start:min(nxt, start + 1600)]
+        stmt = re.split(r':=\s*by|:=\s*$|:=\n|:=\s', body)[0]
+        # signoff window: preceding contiguous comment lines + the decl body up to the next top-level decl.
+        pre = src[:start]
+        lines = pre.split('\n')
+        j = len(lines) - 1
+        if j >= 0 and lines[j].strip() == '':
+            j -= 1
+        k = j
+        while k >= 0 and lines[k].lstrip().startswith('--'):
+            k -= 1
+        comment_block = '\n'.join(lines[k + 1:j + 1])
+        signoff = comment_block + '\n' + src[start:nxt]
+        yield name, stmt, signoff
+
+def flags_for(name, stmt):
+    out = []
+    # Lean identifiers: letters, digits, _, ', unicode subscripts ₀-₉ and Greek/primes
+    ID = r"[A-Za-z0-9_\'₀-₉Ͱ-Ͽ]+"
+    # param vars declared in {..}/(..) of a numeric/complex sort
+    params = re.findall(r'[\{\(]\s*((?:' + ID + r'\s+)*' + ID + r')\s*:\s*(?:ℝ|ℂ|ℕ|ℤ|ℚ)', stmt)
+    pvars = set()
+    for p in params:
+        pvars.update(p.split())
+    pvars = {v for v in pvars if not v.isdigit()}  # drop numeric tokens like "1" from `(1 : ℝ)`
+    # quantifier inversion = BAD (∀var ∃const): a theorem-PARAM var appears in a `≤ c * ...` bound where the
+    # constant c is ∃-bound, and NO inner `∀` re-binds the var between the ∃ and the bound. The GOOD form
+    # (∃c, ∀var, bound) has an inner ∀ after the ∃ and must NOT be flagged.
+    concl = stmt.split(':', 1)[-1]
+    ex = re.search(r'∃\s*(' + ID + r')', concl)
+    if ex:
+        c = ex.group(1)
+        after = concl[ex.end():]
+        le = after.find('≤')
+        seg = after[:le] if le != -1 else after
+        inner_forall = '∀' in seg                      # ∃c ... ∀var ... ≤  => uniform => GOOD, skip
+        bound = re.search(NORM + r'[\s\S]*?≤\s*' + re.escape(c) + r'\s*\*', concl)
+        mentions_param = any(re.search(re.escape(v), concl) for v in pvars)
+        if bound and mentions_param and pvars and not inner_forall:
+            out.append(f"QUANTIFIER-INVERSION: '{name}' is ∀{{{','.join(sorted(pvars))}}} ∃{c} (constant after "
+                       f"variable) — near-vacuous; the genuine form is ∃{c} ∀var. Hoist the ∃ outside the params, "
+                       f"or add a `-- fidelity:` line proving the constant is uniform.")
+    if re.search(r':\s*True\b', stmt) or re.search(r'↔\s*True\b', stmt):
+        out.append(f"TRIVIAL-CONCLUSION: '{name}' concludes `True` — vacuous.")
+    if re.search(r'\(\s*[A-Za-z0-9_\' ]+\s*:\s*False\s*\)', stmt):
+        out.append(f"FALSE-HYPOTHESIS: '{name}' has a `: False` hypothesis — vacuously true.")
+    return out
+
+def main():
+    if len(sys.argv) < 2:
+        print("usage: statement_fidelity_check.py <file.lean> [theorem ...]"); return 2
+    src = open(sys.argv[1], encoding='utf-8', errors='ignore').read()
+    only = set(sys.argv[2:])
+    flagged = 0; checked = 0
+    for name, stmt, signoff in theorems(src):
+        if only and name not in only: continue
+        checked += 1
+        fl = flags_for(name, stmt)
+        signed = bool(re.search(r'--\s*fidelity:', signoff))
+        for f in fl:
+            if signed:
+                print(f"  ok(signed) {f.split(':',1)[0]} on {name} — has -- fidelity: sign-off")
+            else:
+                print(f"  FLAG {f}"); flagged += 1
+    print(f"--- checked {checked} decl(s), {flagged} flag(s)")
+    return 1 if flagged else 0
+
+if __name__ == "__main__":
+    sys.exit(main())