ci(coq-proofs): include docs/phd/theorems/igla/ in verification

[gHashTag]

ci: bring docs/phd/theorems/igla/ under Coq verification

Surgical infrastructure update from GENERAL's Wave-6 follow-up roadmap (item 5 in day-6 status). PR #490 landed INV6_HybridQkGain.v at docs/phd/theorems/igla/ but the existing coq-proofs.yml only watched trinity-clara/proofs/** — every new theorem under the new path silently skipped CI.

Two surgical changes

1. Path triggers

on:
  push:
    branches: [main]
    paths:
      - 'trinity-clara/proofs/**'
      - 'docs/phd/theorems/**'   # ← new
      - '.github/workflows/coq-proofs.yml'
  pull_request:
    branches: [main]
    paths:
      - 'trinity-clara/proofs/**'
      - 'docs/phd/theorems/**'   # ← new

2. New verification step (after the existing INV-1..5 block)

echo "=== docs/phd/theorems/igla/* (Trinity anchor files) ==="
if [ -f docs/phd/theorems/igla/_CoqProject ]; then
  cd docs/phd/theorems
  coq_makefile -f igla/_CoqProject -o igla/Makefile
  make -f igla/Makefile all
  cd -
  echo "✅ docs/phd/theorems/igla/* OK"
else
  echo "(no _CoqProject under docs/phd/theorems/igla — skipped)"
fi

The step uses the existing _CoqProject at docs/phd/theorems/igla/ which is already wired with -R trinity Trinity / -R igla IGLA. Wrapped in an [ -f ... ] guard so the step degrades gracefully if the project file is later removed.

R5-honest disclosures

• This change alone does not verify INV6_HybridQkGain.v is a parseable proof. It only points CI at the file. The first run on main after this PR merges is the binding verification.
• If coq_makefile / make all discovers any unprovable goal — for instance, if PR feat(coq): INV6_HybridQkGain.v — formal proof skeleton, closes #441 #490's residual Axiom hybrid_gain_phi_bound plus the proof script combine into something coqc rejects — CI will go RED and the scaffold will need follow-up before the next push to main.
• The Check no Admitted in proofs (L-R14 strict) gate downstream still only inspects trinity-clara/proofs/igla/*.v. If that should now also cover docs/phd/theorems/igla/*.v, that's a separate diff (would catch any Admitted. regression in the new path).

Honest scope

This is the CI infrastructure piece of the post-#490 roadmap. It does not include:

• The actual proof PR that replaces Axiom hybrid_gain_phi_bound with a sqrt_le_compat derivation (PR ci(coq-proofs): include docs/phd/theorems/igla/ in verification #491, deferred — sandbox lacks coqc so speculative Coq would fail the same R5 review I issued on PR feat(coq): INV6_HybridQkGain.v — formal proof skeleton, closes #441 #490 itself).
• A fix for the pre-existing crates/trios-phd/src/main.rs clippy doc-overindent lint that's keeping the Audit · Biblio · Coq-map · Reproduce job red.

Both tracked separately.

CI honest disclosure

Pre-existing failures on main (I5 red on legacy crates/trios-a2a/rings/* and crates/trios-mcp/rings/*, ARCH-UI, generic Test, phd-build clippy doc-lint) remain out of scope. Merge via --admin --squash --delete-branch per EPIC #446 stewardship.

Part-of: #441
Part-of: #446
Follow-up to: PR #490 (merged at ff02df9)

🌻 α_φ = φ⁻³/2 ≈ 0.1180 · φ²+φ⁻²=3 · TRINITY · LEAD (Loop-Locksmith)