gHashTag · gHashTag · May 13, 2026
diff --git a/README.md b/README.md
@@ -21,18 +21,55 @@ This repository contains formal specifications, evidence packages, working examp
 
 ### Key Differentiation
 
-1. **Formal Adversarial Robustness** — Unique among SOA systems with 100% Red Team success across 5 attack categories
-2. **84 Coq Theorems** — Most comprehensive formal verification pipeline (.t27 → Verilog)
+1. **Formal Adversarial Robustness** — 100% Red Team success across 5 attack categories (50/50 cases, see [`evidence/CLARA-RED-TEAM.md`](evidence/CLARA-RED-TEAM.md))
+2. **Formal proof-backed cognitive substrate** — IGLA proof bundle: **47 Qed, 4 Admitted, 1 honest placeholder, 1 axiom, 10 falsification witnesses** across 8 `.v` files (see [`proofs/igla/_metadata.json`](proofs/igla/_metadata.json) and [`docs/TRINITY_PHD_PROVENANCE.md`](docs/TRINITY_PHD_PROVENANCE.md)). Upstream `t27` proof base (audit 2026-05-12): 28 `.v` files, 218 stated Theorem/Lemma, **162 Qed / 32 Admitted / 2 Abort**.
 3. **Guaranteed Polynomial Bounds** — All operations with formal Big-O proofs
 4. **Ternary Logic K3** — CLARA restraint compliant (UNKNOWN→FALSE bounded rationality)
 5. **GF16 Encoding** — φ-optimized 65,000× wider dynamic range, 1.8× more accurate than float
-6. **Energy Efficiency** — 49× better than GPU (native FPGA implementation)
+6. **Energy Efficiency** — 49× better than GPU (native FPGA implementation, XC7A100T prototype)
 7. **Vector Symbolic Architecture** — 1024-dimensional ternary hypervectors with theoretical foundations
 
+> **Honest scoping note.** This repository is a *submission slice*, not the full upstream proof base. The IGLA proof bundle shipped here is **not** fully proven — it is honestly partial (4 declared `Admitted` obligations with stated closure paths, 1 `Qed`-placeholder bound to a runtime guard, 1 axiom). The phrase "84 Coq theorems" that appears in some older v1.x narrative is a historical v1.1 snapshot and is superseded by the counts in [`docs/TRINITY_PHD_PROVENANCE.md`](docs/TRINITY_PHD_PROVENANCE.md).
+
 **Migration Notice:** This repository was extracted from [t27](https://github.com/gHashTag/t27) on 2026-04-15 to isolate the DARPA submission from the main Trinity codebase.
 
 ---
 
+## Proof Artifacts, Provenance, and Upstream Repositories
+
+**Read first:** [`docs/TRINITY_PHD_PROVENANCE.md`](docs/TRINITY_PHD_PROVENANCE.md) — the canonical, auditable provenance appendix for this submission. Everything below is a pointer.
+
+### Coq proof artifacts (this repo)
+
+| Artifact | Path | Status |
+|---|---|---|
+| IGLA proof bundle (metadata) | [`proofs/igla/_metadata.json`](proofs/igla/_metadata.json) | 8 files, 47 Qed, 4 Admitted, 1 placeholder, 1 axiom, 10 falsification witnesses |
+| IGLA `.v` sources | [`proofs/igla/`](proofs/igla/) | `igla_asha_bound.v`, `gf16_precision.v`, `nca_entropy_band.v`, `lr_convergence.v`, `lucas_closure_gf16.v`, `igla_found_criterion.v`, `bpb_monotone_backward.v`, `hybrid_qk_gain.v`, `CorePhi.v` |
+| Runtime invariant contract | [`assertions/igla_assertions.json`](assertions/igla_assertions.json) | Machine-readable binding from `proofs/igla/*.v` to runtime checks (L-R14) |
+
+### Upstream Trinity repositories
+
+| Repository | Role |
+|---|---|
+| [`gHashTag/t27`](https://github.com/gHashTag/t27) | `.t27` compiler, Verilog backend, broader Coq proof base. Audit 2026-05-12: 28 `.v` files, 218 stated Theorem/Lemma, **162 Qed / 32 Admitted / 2 Abort**. |
+| [`gHashTag/trios`](https://github.com/gHashTag/trios) | PhD-thesis source (`docs/phd/`), Rust audit harness (`crates/trios-phd/`), runtime invariant contracts. Relevant issues: [trios#372](https://github.com/gHashTag/trios/issues/372), [trios#264](https://github.com/gHashTag/trios/issues/264). |
+
+### PhD provenance
+
+The Trinity S³AI architecture has a PhD-thesis backbone in `gHashTag/trios:docs/phd/`. CLARA-relevant chapters and appendices (by topic): **Ch. 22** (proof discipline / invariant contracts), **Ch. 24** (φ-structured arithmetic and GF16), **Ch. 28** (compositional reasoning, L1–L7), **Ch. 34** (IGLA / RACE), plus appendices **App. B / F / G / H / I / M / N**. The canonical paths are whatever is checked in to `trios:docs/phd/` at the audit cutoff; we do not duplicate the PhD source tree here. See [`docs/TRINITY_PHD_PROVENANCE.md`](docs/TRINITY_PHD_PROVENANCE.md) §4.
+
+### Software & provenance DOIs (Zenodo)
+
+Zenodo records are **provenance / citation handles for software releases**, not a proof source. The proof source is `proofs/igla/*.v` (this repo) and the upstream `t27` Coq base.
+
+| DOI | Subject |
+|---|---|
+| [10.5281/zenodo.19227879](https://doi.org/10.5281/zenodo.19227879) | TRINITY framework (umbrella) |
+| [10.5281/zenodo.19227877](https://doi.org/10.5281/zenodo.19227877) | φ / VSA components |
+| [10.5281/zenodo.18947017](https://doi.org/10.5281/zenodo.18947017) | FPGA / hardware backend |
+
+---
+
 ## Quick Start
 
 ### Installation
@@ -309,10 +346,14 @@ Dr. Scott A. Olsen, Ph.D. (Philosophy, University of Florida), J.D. (Levin Colle
 
 ### Co-Investigator — Dmitrii Vasilev (Trinity S³AI Research Group)
 
-Mr. Vasilev leads the Trinity S³AI research effort that underpins this proposal. He is the primary architect of the Trinity/t27 mathematical framework, which unifies a φ-structured number system, a compositional reasoning calculus (L1–L7 derivation hierarchy), and a formally verified library of 80+ Coq theorems (Rocq 9.1.1) relating golden-ratio-based invariants to computable reasoning procedures. His prior work includes: (1) design and implementation of the t27 compiler and GoldenFloat formats (Zig/Verilog/C backends) for hardware-amenable φ-arithmetic; (2) development of the Chimera search system that composes analytical reasoning (AR) and machine learning (ML) into verifiable search pipelines; and (3) end-to-end Coq proofs demonstrating polynomial-time tractability and soundness for key fragments of the Trinity calculus. Within CLARA, he is responsible for the formal specification, proof engineering, and reference implementations that realize compositional learning-and-reasoning as a verifiable, end-to-end pipeline rather than a black-box model.
+**ORCID:** [0009-0008-4294-6159](https://orcid.org/0009-0008-4294-6159) · **Upstream artifacts:** [`gHashTag/t27`](https://github.com/gHashTag/t27), [`gHashTag/trios`](https://github.com/gHashTag/trios), [`gHashTag/trinity-clara`](https://github.com/gHashTag/trinity-clara).
+
+Mr. Vasilev leads the Trinity S³AI research effort that underpins this proposal. He is the primary architect of the Trinity/t27 mathematical framework, which unifies a φ-structured number system, a compositional reasoning calculus (L1–L7 derivation hierarchy), and a Coq proof base (Rocq 9.1.1) relating golden-ratio-based invariants to computable reasoning procedures. As of the **2026-05-12 audit** of upstream `t27`, that proof base has 28 audited `.v` files with 218 stated Theorem/Lemma — **162 Qed / 32 Admitted / 2 Abort**; the CLARA-scoped IGLA subset shipped here is documented in [`docs/TRINITY_PHD_PROVENANCE.md`](docs/TRINITY_PHD_PROVENANCE.md) and [`proofs/igla/_metadata.json`](proofs/igla/_metadata.json). His prior work includes: (1) design and implementation of the t27 compiler and GoldenFloat formats (Zig/Verilog/C backends) for hardware-amenable φ-arithmetic; (2) development of the Chimera search system that composes analytical reasoning (AR) and machine learning (ML) into verifiable search pipelines; and (3) Coq proofs demonstrating polynomial-time tractability and soundness for key fragments of the Trinity calculus (with `Admitted` budgets and closure paths tracked explicitly per `L-R14`). Within CLARA, he is responsible for the formal specification, proof engineering, and reference implementations that realize compositional learning-and-reasoning as a verifiable, end-to-end pipeline rather than a black-box model.
 
 ### Co-Investigator — Dr. Stergios Pellis (Physics & Applied Mathematics)
 
+<!-- TODO (pre-submission): confirm institutional affiliation and ORCID for Dr. Pellis. Not yet recorded; do not invent. -->
+
 Dr. Pellis contributes expertise in mathematical physics, statistical validation, and experimental design. He has worked on formalizing and statistically validating Trinity S³AI's φ-structured constants and invariants, including large-scale significance studies (e.g., p-values on the order of 10⁻⁵³ across dozens of formulas) that distinguish genuine structure from numerology. In the present project, Dr. Pellis leads the design of benchmark suites and ablation studies that compare Trinity-style compositional reasoning against existing neuro-symbolic baselines, ensuring that claimed advantages are supported by rigorous experimental evidence, confidence intervals, and reproducible test harnesses rather than anecdotal examples.
 
 ### Collective Capability

diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
@@ -342,11 +342,12 @@ Memory Resources:
 - Formal guardrails at all pipeline stages
 - <10ms recovery time guaranteed
 
-### 2. 84 Coq Theorems
-**Most Comprehensive:** Complete formal verification path
-- .t27 specifications → Verilog synthesis
-- Semantic preservation guaranteed
-- All operations verified mathematically
+### 2. Coq Proof Base
+**Honest, audited formal verification:**
+- IGLA bundle (`proofs/igla/`, this repo): 47 Qed, 4 Admitted (with stated closure paths), 1 honest `Qed`-placeholder, 1 axiom, 10 falsification witnesses across 8 `.v` files
+- Upstream `t27` Coq base (audit 2026-05-12): 162 Qed / 32 Admitted / 2 Abort across 28 `.v` files
+- `.t27` specifications → Verilog synthesis with semantic preservation
+- See [`TRINITY_PHD_PROVENANCE.md`](TRINITY_PHD_PROVENANCE.md) for full provenance
 
 ### 3. GF16 Confidence Encoding
 **φ-Optimized:** 1.618... constant for optimal range

diff --git a/docs/FAQ.md b/docs/FAQ.md
@@ -329,7 +329,7 @@ See `evidence/CLARA-LITERATURE-REVIEW.md` for 12 foundational papers.
 
 **A:** TRINITY CLARA differs from NeSy in several key aspects:
 
-1. **Formal Verification** — TRINITY includes 84 Coq theorems and .t27 → Verilog path, providing hardware correctness guarantees that most NeSy systems lack.
+1. **Formal Verification** — TRINITY includes an auditable Coq proof base (IGLA bundle in `proofs/igla/`: 47 Qed / 4 Admitted / 1 honest placeholder / 1 axiom + 10 falsification witnesses across 8 `.v` files; upstream `t27` audit 2026-05-12: 162 Qed / 32 Admitted / 2 Abort across 28 `.v` files) plus a `.t27` → Verilog path, providing hardware correctness guarantees that most NeSy systems lack. See [`TRINITY_PHD_PROVENANCE.md`](TRINITY_PHD_PROVENANCE.md).
 
 2. **Explicit Restraint** — TRINITY uses K3 logic with explicit UNKNOWN value for bounded rationality, whereas NeSy often uses soft constraints.