Caution
No Theory-of-Everything claim is made. This repository documents an active boundary-mapping research program β we prove what H4 geometry cannot reproduce, narrowing the search space.
| Role | Start here | Time | What you'll learn |
|---|---|---|---|
| Physicist / Reviewer | docs/REVIEW_GUIDE.md |
10 min | Honest path with commands and expected outputs |
| Formal methods researcher | proofs/trinity/BoundaryTheorems.v |
5 min | BT-1..BT-4 Qed; 51 unproven obligations (0 real Admitted + 51 Axiom/Parameter/Conjecture) across 56 Coq files in proofs/trinity/ |
| Curious visitor | π GOLDEN CHAIN live | 2 min | Hardware-verified proof chain puzzle |
| Contributor | CONTRIBUTING.md + good first issue |
15 min | Build instructions, phi-loop protocol |
Most unification programs publish only successes. We publish the dead ends too β because a formally proven dead end saves the field from years of wasted effort.
| Our Strong Side | What It Means For You |
|---|---|
1,325 theorems with Qed. |
Every positive claim is machine-checked (~210 are trivial/tautological; ~1,100 are substantive). |
| 4 boundary theorems (BT-1..BT-4) | Four direct H4βSM construction paths are formally ruled out. You don't have to try them. |
| 14 refutation theorems | Specific ansΓ€tze (orbifold Zβ, E8-plumbing Ξ·, Ξ΄_CP = 65.66Β°) are proven dead and documented. |
0 real Admitted. + 51 obligations in proofs/trinity/ |
No cosmetic edits. Every open gap is an Axiom/Parameter with a literature citation. See COQ_HONEST_STATUS.md for full accounting. |
| 0 fake proofs | The honest parser strips comments before counting. Naive grep finds 77; the real count is 0 in proofs/trinity/. |
$TRI is not a cryptocurrency. It is a compression score (bits-per-byte) benchmarked on synthetic Ο-structured data; silicon validation is NOT pending: the TTSKY26b submission (2026-05-17) was withdrawn and refunded, so no die will be returned. You cannot mine it on a GPU.
We maintain a catalog of 130 total formulas/invariants (59 SM-sector phenomenological formulas) between H4 Coxeter invariants and PDG 2024 measurements, plus 4 formal boundary theorems proving obstructions. Whether the coincidences are deep or accidental is itself an open research question β tracked via a 7-layer verification stack and a living claim ledger.
| Layer | Status | Key Metric | Details |
|---|---|---|---|
| L0 Infrastructure | β | Live demo | Rust + Coq CI, anti-numerology gate |
| L1 Claim Ledger | β | SSOT claims.yaml |
5-status vocabulary enforced |
| L2 Formal Proofs | β | 0 real Admitted in proofs/trinity/ | 51 unproven obligations (Axiom/Parameter/Conjecture) in proofs/trinity/ |
| L3 Geometry | aβ factor unresolved |
3 derivations don't converge | |
| L4 NCG / Lagrangian | π΄ | BT-2, BT-6 bound recovery | No Ο-field from H4; no string rescue |
| L5 Numerical Fits | 59 formulas, 1 withdrawn | Ξ΄_CP withdrawn; sinΒ²ΞΈ_W = 84Ο genuine failure | |
| L6 GOLDEN CHAIN | β | Rust + wasm deployed | 5-ring Cargo workspace |
| L7 Publication | π | Paper v2 in prep | arXiv + Zenodo pipeline |
flowchart BT
L7["L7 Publication: paper v2 / arXiv / Zenodo"] --> L6
L6["L6 GOLDEN CHAIN: silicon-targeted chain"] --> L5
L5["L5 Numerical Fits: 59 formulas, p-values"] --> L4
L4["L4 NCG / Lagrangian: spectral action"] --> L3
L3["L3 Geometry: H4 / 600-cell / Cl(8)"] --> L2
L2["L2 Formal Proofs: Coq / Lean, BT-1..BT-4"] --> L1
L1["L1 Claim Ledger: 5-status SSOT"] --> L0
L0["L0 Infrastructure: CI, honest counter, Pages"]
style L2 fill:#90EE90,stroke:#333
style L5 fill:#FFD700,stroke:#333
style L4 fill:#FF6B6B,stroke:#333
style L3 fill:#FFD700,stroke:#333
| Theorem | Statement | What It Closes |
|---|---|---|
| BT-1 (Cosmology) | Οα΅ Οα΅ eαΆ formulas cannot reproduce Ξ or Ξ©_b | Algebraic ansΓ€tze for cosmological constants from H4 invariants are dead ends. |
| BT-2 (Ο-field) | No NCG Ο-field from H4 root structure alone | Direct NCG spectral-action derivation from H4 geometry alone is impossible; redirects to Cl(8) / Jβ(π). |
| BT-3 (Chirality) | 600-cell D_F is vector-like (antipodal symmetry) | The 600-cell cannot source SM chirality; chirality must enter via a different mechanism. |
| BT-4 (Mass hierarchy) | 2I-equivariant D_F cannot reproduce lepton mass ratios | Icosahedral symmetry-breaking ansatz for lepton masses is insufficient; needs stronger breaking. |
Coq Stats (Wave 23): 1,325 theorems with Qed. (~210 trivial, ~1,100 substantive) Β· 0 real Admitted. + 51 unproven obligations (Axiom/Parameter/Conjecture) in proofs/trinity/ Β· 14 refutation theorems
Honest p-value: p = 0.077 (mean error, not significant) Β· p < 0.0001 (SG-hit density, significant)
"Not a proof is also a proof." β We share what we tried to prove and could not, because knowing the boundary is as valuable as knowing the path.
Real training results on FineWeb-Edu 10B token subset, 196K-parameter transformer (hidden=384, 2 attention layers, AdamW lr=0.003). Lower BPB = better compression.
Champion (no quantization, seed=43, 81K steps): best = 2.3900 [empirical_fit]
| Format | Best BPB @ 10K | Best BPB @ 40β50K | Verdict |
|---|---|---|---|
| bf16 | 2.7127 | β | Reference |
| fp16 | 2.7183 | 3.0383 @ 50K | Reference |
| f32 | 2.7375 | 3.0391 @ 50K | Reference |
| gf16 | 2.7186 | 3.0260 @ 50K | Matches 16-bit baseline |
| posit8 | 3.0099 | 2.9737 @ 40K | Competitive at medium steps |
| gf8 | 3.0099 | 2.9737 @ 40K | Competitive at medium steps |
| mxfp8 | 3.3874 | ~3.5 | Marginal |
| int8 | 3.6092 | ~3.9 | Marginal |
| nf4 | 3.8659 | ~4.0 | Marginal |
| fp8_e5m2 | 4.5309 | β | Non-viable |
| int4 | 7.0005 | ~7.0 | Non-viable |
Key finding [empirical_fit]: GF16 matches fp16/f32 compression despite Ο-structured mantissa β no accuracy penalty at 16-bit precision on language modeling.
Surprise [empirical_fit]: posit8 and gf8 (8-bit formats) outperform 16-bit fp16/f32 at 40β50K steps, suggesting Ο-aware quantization may stabilize optimization beyond naive bit-width expectations.
Dead formats [verified β refutation]: int4 and fp8_e5m2 fail to converge below 4.5 BPB on this architecture β empirically ruled out for the 196K-param regime.
Raw logs: trios-trainer-igla/.trinity/results/ β see trios-trainer-igla.
The Trinity SΒ³AI knowledge chain is designed to anchor in silicon. $TRI (Trinity Index) is the project's native proof-of-work metric β not a cryptocurrency, but a compression score measured in bits-per-byte (BPB) on Ο-structured arithmetic. Hardware validation is pending.
Coq Qed. Silicon 0x47C0 Boundary Theorem
| | |
v v v
+-------------------+ +-----------------------+ +------------------------+
| Formal proof of | | Lucas chain L2 = 3 | | BT-1..BT-4 prove which |
| 1,762 theorems | | anchored in GF(16) | | H4βSM paths are closed |
| (Track A + B) | | submitted for TTSKY26b | | (saves field from blind |
| | | | | alleys) |
+-------------------+ +-----------------------+ +------------------------+
| | |
+------------+------------+------------+-------------+
|
v
+---------------------+
| GOLDEN CHAIN score |
| = silicon-targeted |
| proof-of-work |
+---------------------+
Every link is independently auditable: the Coq side builds in CI, the silicon anchor is submitted for TinyTapeout fabrication, and the boundary theorems are in BoundaryTheorems.v with Qed.
| Crown | Chip | Tile | Modules | Anchor | Role |
|---|---|---|---|---|---|
| Phi (Nano) | tt_um_trinity_nano |
1Γ1 | 51 | 0xCF |
Minimal-area witness |
| Euler (Compact) | tt_um_ghtag_trinity_gf16 |
8Γ2 | 90 | 0xAE |
GF(16) Galois-field carrier |
| Gamma (Full) | tt_um_trinity_max_true |
8Γ4 | 105 | 0x93 |
Full Trinity-SΒ³AI DNA |
All three crowns are designed to carry the canonical anchor 0x47C0 at {uio_out, uo_out} on reset β a planned silicon witness of ΟΒ² + Οβ»Β² = 3 via the Lucas chain Lβ = 3 β GF(16) dot4 trace. Post-silicon logic-analyzer validation is pending (see docs/hardware/silicon_anchor.md Β§3.3).
- Ο-structured step: each quantization level approximates
Οβ»ΒΉ β 0.618, giving 0.694-bit reduction per level (mathematical identityβ logβ Ο identity; Prop 1β2, Thm 3 ingf16_mathematics.md) - 16.2Γ better than bf16 on uniform data: 9-bit mantissa vs bf16's 7 bits (
empirical_fitβ zig-golden-float BENCH-010 Uniform [-100,100]) - 65Γ wider dynamic range than fp16: max normal ~4.29Γ10βΉ vs fp16's 65504; exact powers-of-two at
-120.00 dBNMSE (empirical_fitβbenchmark_nmse.pyD-5) - Zero inference accuracy drop: Fashion-MNIST MLP post-training quantization = 0.00% drop vs fp32 (
empirical_fitβ zig-golden-float BENCH-008) - Optimal integer Ο-split:
round((Nβ1)/ΟΒ²)gives exp=6/mant=9 for N=16; phi-distance 0.049 vs fp16 0.118 (proposedβ NeurIPS 2026 OPT Prop 2; not yet peer-reviewed) - Hardware exclusivity: WITHDRAWN β the TTSKY26b submission (Three Crowns: Phi + Euler + Gamma) was withdrawn and refunded; no silicon route is currently selected
Honest note on BPB: GF16 is a 16-bit float, so raw BPB = 0.500 β identical to fp16 and bfloat16 by bit-width. The 0.125 raw BPB claim belongs to the separate phi-4Q 4-bit quantizer (synthetic Ο-structured data only). See
docs/hardware/bpb_benchmark.pyanddocs/hardware/gf16_mathematics.mdΒ§2.2.
~1 GOPS @ ~50 MHz @ ~1 W ternary (projected on QMTech XC7A100T).
This project is built on a counter-intuitive principle: proving what cannot be done is as valuable as proving what can.
| What we proved | Count | Status |
|---|---|---|
Theorems with Qed. |
1,325 (~210 trivial, ~1,100 substantive) | Verified |
| Boundary theorems (impossibility proofs) | 4 (BT-1..BT-4) | Verified |
Refutation theorems (*_refuted) |
14 | Verified dead ends |
Real Admitted. (outside comments/strings) |
0 in proofs/trinity/ | Verified by honest parser |
| Fake proofs | 0 | β |
Boundary theorems save the field from wasted effort:
- BT-1 β no
Ο^a Ο^b e^cmonomial can reproduce cosmological constants β saves theorists from algebraic dead ends - BT-2 β no NCG Ο-field from H4 alone β redirects toward Cl(8) / Jβ(π) constructions
- BT-3 β 600-cell Dirac operator is vector-like β chirality must come from elsewhere
- BT-4 β 2I-equivariant D_F fails for lepton masses β mass hierarchy needs different symmetry breaking
0 real Admitted gaps in proofs/trinity/ β the honest parser strips comments before counting. Naive grep finds 5 mentions in comments; the real count is 0. Total unproven obligations in proofs/trinity/: 51 (Axiom/Parameter/Conjecture).
0 fake proofs. 0 cosmetic edits to hide gaps. Every number is produced by a comment-stripping parser and treated as ground truth.
# Docker (zero dependencies)
docker run -it --rm -v $(pwd):/work coqorg/coq:8.20.1 bash -c \
"cd /work/proofs/trinity && coq_makefile -f _CoqProject -o Makefile.coq && make -f Makefile.coq -j$(nproc)"
# Validators
pip install mpmath numpy
python3 scripts/validators/validate_v4.py
python3 scripts/anti_numerology_gate.py
python3 scripts/count_admitted_honest.pyFull build matrix: docs/BUILD.md Β· Contributing: CONTRIBUTING.md
You do not have to trust our numbers. Run these four commands in order:
# 1. Anti-numerology gate β checks that every Ο/Ο/e formula is honesty-tagged (~5 s)
python3 scripts/anti_numerology_gate.py
# Expected: VERDICT: PASS
# 2. Honest Coq counter β strips comments before counting Admitted (~2 s)
python3 scripts/count_admitted_honest.py
# Expected: proofs/trinity/ β 0 real Admitted + 51 Axiom/Parameter/Conjecture; 56 .v files.
# 3. Formula error bounds β verifies numeric claims against PDG 2024 (~10 s)
pip install mpmath numpy
python3 scripts/validators/validate_v4.py
# Expected: error claims match the table below
# 4. GOLDEN CHAIN ring-boundary tests β checks inward-only dependency (~30 s)
cd games/trinity_fold && cargo test --workspace
# Expected: all tests pass, including ring_boundaries.rsIf any step fails, the README statistics are stale β please open an issue.
@software{trinity_s3ai_2026,
title = {Trinity-s3ai: Active Boundary-Mapping Research Program},
author = {Dmitrii Vasilev},
year = {2026},
url = {https://github.com/gHashTag/trinity-s3ai},
note = {v1.0-wave23}
}See CITATION.cff for metadata. Zenodo DOI badge pending deposit.
π Full Claim Ledger (auto-generated from claims.yaml)
Generated from docs/claims.yaml by scripts/generate_claims.py. Do not edit this block by hand.
| Claim | Layer | Status | Evidence | Blocking gap |
|---|---|---|---|---|
| GOLDEN CHAIN live canvas deployed on GitHub Pages (Rust + wasm) | L0 | verified |
.github/workflows/pages.yml; live at https://t27.ai/trinity-s3ai/ | β |
Wave 17 honest counter reports 0 real Admitted. in proofs/trinity/ |
L2 | verified |
scripts/count_admitted_honest.py output; HONESTY_MANIFEST.md | Holds only for proofs/trinity/. Track B (proofs/clifford_cl8/) retains load-bearing Axioms with citations; the Lagrangian derivation is not closed. |
BT-1βBT-4: four formal Boundary theorems closed with Qed. |
L2 | verified |
proofs/trinity/BoundaryTheorems.v (BT1, BT2, BT3, BT4 all Qed) | β |
| E8 plumbing: eta discrepancy does NOT converge to -2 | L4 | high_risk_or_falsified |
paper/CHANGELOG_v1_to_v2.md (Honesty Notes); Wave 17 audit | β |
| No known string / heterotic / F-theory / orbifold compactification rescues the SM hierarchy from H4 or F4 | L4 | high_risk_or_falsified |
ROADMAP_WAVE17_PLUS.md (Wave 17.2 Findings) | β |
a4 conversion factor not fully reconciled across three derivations |
L3 | open_conjecture |
docs/analysis/a4_conversion_factor_analysis.md; docs/analysis/a4_honest_resolution.md | Produce a single derivation that all three (analytic, spectral, fit) paths agree on, or document why they cannot agree and downgrade the relevant fits. |
m_H = 4 phi^3 e^2 ~ 125.1 GeV is the Higgs mass |
L5 | empirical_fit |
proofs/trinity/HiggsPrediction.v (interval bound); docs/analysis/higgs_potential_proven.md | Derive m_H from H4 / NCG structure rather than from a (phi, e) monomial. Any such derivation must pass the anti-numerology gate and avoid the BT2 sigma-field boundary. |
| GOLDEN CHAIN puzzle is a silicon-targeted proof chain, not evidence | L6 | verified |
games/trinity_fold/README.md; ring0_core::ClaimStatus enum | β |
| No Theory-of-Everything claim and no prize claim is made | L1 | verified |
docs/CLAIM_STATUS.md Β§2; README.md preamble | β |
| GF16 (1-6-9, bias 31) phi-anchored float format specified and FPGA-verified | L0 | verified |
docs/hardware/gf16_spec.md Β§2β2.6; t27/conformance/FORMAT-SPEC-001.json; NeurIPS 2026 OPT paper (Prop 1β2, Thm 3); IBM DLFloat16 (ARITH 2019, layout identical, 6 differences documented) | β |
| BPB compression benchmark: phi-4Q quantizer raw BPB 0.125 vs 0.500 for fp16/bf16/GF16 | L5 | empirical_fit |
docs/hardware/bpb_benchmark.py; docs/hardware/bpb_results.json (generated 2026-05-25) | Extend benchmark to real physics datasets (e.g. PDG parameter vectors, MNIST weights) and verify the advantage persists outside synthetic phi-monomial data. |
| IGLA RACE champion: f32 baseline BPB = 2.3900 on 81K steps (196K params) | L5 | empirical_fit |
trios-trainer-igla/.trinity/results/champion_81k_seed43.log; seed=43, hidden=384, 2 attn layers, AdamW lr=0.003 | Reproduce on independent hardware and confirm the BPB floor is stable across seeds. Run seeds 44β50 to 81K with identical hyperparameters. |
| IGLA RACE: GF16 matches fp16/f32 BPB on language modeling (empirical parity) | L5 | empirical_fit |
trios-trainer-igla/.trinity/results/v2_gf16_seed44_81k.log (ema_bpb=3.0260 @ 50K); v2_fp16_seed44_81k.log (ema_bpb=3.0383 @ 50K); v2_f32_seed42_81k.log (ema_bpb=3.0391 @ 50K) | Run GF16 to 81K steps (currently only 50K available) and verify the parity holds at full convergence. Run multiple seeds to bound variance. |
| IGLA RACE: posit8 and gf8 outperform 16-bit baselines at 50K steps (surprise) | L5 | empirical_fit |
trios-trainer-igla/.trinity/results/v2_posit8_seed44_50k.log (ema_bpb=2.9737 @ 40K); v2_gf8_seed44_50k.log (ema_bpb=2.9737 @ 40K) | Extend to 81K steps and multiple seeds. Verify the advantage is not a seed artifact. Compare against int8 to isolate phi-aware benefit. |
| IGLA RACE: int4 and fp8_e5m2 non-viable on 196K-param transformer | L5 | high_risk_or_falsified |
trios-trainer-igla/.trinity/results/v3_int4_seed46_10k.log (ema_bpb=7.0005); v3_fp8_e5m2_seed47_10k.log (ema_bpb=4.5309) | β |
| Ο-anchored hyperparameters falsified on IGLA RACE: +0.1013 BPB worse than conventional | L5 | high_risk_or_falsified |
docs/audit/PHI_ABLATION_DESIGN.md; trios-trainer-igla/.trinity/gardener_harvest.log (control best=2.6167, treatment best=2.7180) | β |
| GF16 silicon tapeout on TinyTapeout TTSKY26a shuttle (submitted, pending silicon) | L0 | open_conjecture |
docs/hardware/silicon_anchor.md Β§3.1; PR #322 in TinyTapeout/tinytapeout-sky-26a for gHashTag/tt-trinity-gf16 | Await silicon return from Sky130 fab (~Aug 2026). Post-silicon validation requires logic-analyzer reset witness, clock sweep, and conformance run. |
| 0x47C0 reset-time silicon anchor validates Lucas chain L2=3 | L0 | open_conjecture |
docs/hardware/silicon_anchor.md Β§1β2; no RTL testbench found in t27 repo | Document the anchor in RTL (add reset witness to gf16_mul.v or wrapper), add testbench simulation, or downgrade claim to design-intent only. |
| phi-structured quantization step gives ~0.694-bit reduction per level | L3 | verified |
docs/hardware/gf16_mathematics.md Β§3, Β§6.1β6.3; log2(phi) = 0.6942419136...; NeurIPS 2026 Prop 1 (Golden Self-Similarity), Prop 2 (Optimal Integer Rounding), Thm 3 (Universal Attractor) | β |
| Coq/Flocq proof: phi^2 = phi + 1 holds exactly in IEEE binary64 | L2 | verified |
proofs/trinity/PhiFloat.v (adapted from t27/coq/Kernel/PhiFloat.v); phi_sq_f64 = phi_plus_one_f64 by vm_compute; residual 0.0 < tolerance 1e-15 | Extend to GF16: prove phi identity holds (or bound error) in the 1-6-9 format. Currently proved only for binary64, not for GF16. |
| Three Crowns (Phi/Euler/Gamma) submitted to TinyTapeout TTSKY26b | L0 | open_conjecture |
docs/hardware/silicon_anchor.md Β§3.2; 21 closed PRs in TinyTapeout/tinytapeout-sky-26b (9 phi + 7 euler + 5 gamma) | Await silicon return from Sky130 fab (~Nov 2026). Post-silicon validation of all three crowns required before upgrade to verified. |
| The weight alphabet base is forced: any r > 1 with r*r = r + 1 is phi | L1 | verified |
derivations/golden_alphabet/GoldenAlphabet.v: phi_quadratic, phi_unique (Qed, coqchk clean, negative control run) | β |
| Multiplying by phi on integer pairs is the Fibonacci step: one addition, no shift | L1 | verified |
derivations/golden_alphabet/GoldenAlphabet.v: mulphi_correct, addp_correct, negp_correct (Qed) | β |
| The linear path of a {-phi, 0, +phi} network is exact at any fan-in and depth | L1 | verified |
derivations/golden_alphabet/GoldenAlphabet.v: dot_exact (Qed); Z[phi] closure | Rounding still enters at the nonlinearity; that is outside this statement. |
| The gain of k stacked phi-ternary layers is F_(k+1)*phi + F_k, a pair of integers | L1 | verified |
derivations/golden_alphabet/GoldenAlphabet.v: phi_pow_fib (Qed, by induction) | β |
To update: edit docs/claims.yaml, run python3 scripts/generate_claims.py,
commit both the YAML and the regenerated artefacts. CI runs the same
script with --check and fails if anything is stale.
π Wave History
| Wave | Key addition |
|---|---|
| 1β3 | Initial Ο/Ο/e formula catalog |
| 4.1 | Honesty tags: [phenomenological_fit], [NUMERICAL_FIT] added |
| 5β8 | NCG derivations, spectral action |
| 9.6 | BT-1βBT-4 boundary theorems formalized |
| 10.5 | Anti-numerology CI gate; CITATION.cff; CONTRIBUTING.md |
| 12 | Track B launch: Cl(p,q) formalization (T1βT3) |
| 15.1 | Honest counting system: comments stripped before statistics |
| 17 | Formal retraction of Ξ΄_CP = 65.66Β° (5.6Ο excluded); 0 real Admitted. in proofs/trinity/ |
| 18 | Merge of honesty-pass PRs #21β#23 (Lagrangian status, Ξ΄_CP withdrawal, Coq audit) |
| 19 | Merge of honesty-pass PRs #29, #31, #32 (calculation-primacy, N_gen=3 withdrawn, Strong CP withdrawn); all old PRs merged |
| 20 | Honest phenomenology refresh: 500k-trial p-value, Ο-ranking updated (26 obs, Ξ΄_CP withdrawn, sinΒ²ΞΈ_13/23/W + |V_ub| + Ξ» added) |
| 23 | README redesign: lean structure, audience selector, Mermaid tech tree, collapsible ledger |
| 24 | Ο falsifiability ablation: Ο-anchored hyperparameters falsified (+0.1013 BPB worse than conventional) β see docs/audit/PHI_ABLATION_DESIGN.md |
| 25β28 | Queued: Coq gap closure (Wave 25), IGLA Gate-2 push (Wave 26), Lean 4 port (Wave 27), GOLDEN CHAIN integration (Wave 28) β see docs/WAVES_24_28.md |
| Resource | Description |
|---|---|
docs/REVIEW_GUIDE.md |
For reviewers: 10-minute path with commands and expected outputs |
docs/REPOSITORY_MAP.md |
Where every kind of artifact lives |
docs/CLAIM_STATUS.md |
Claim-status rule book (5 canonical statuses) |
docs/TECH_TREE.md |
Layered status of the whole stack |
RESEARCH_STATUS.md |
Boundary map: open, obstructed, or under exploration |
docs/WAVES_24_28.md |
Next waves: IGLA RACE, Coq gaps, Lean port, game integration |
HONESTY_MANIFEST.md |
Ground-truth statistics (comments stripped) |
ROADMAP_WAVE17_PLUS.md |
Tracks A, B, C of active research |
paper/CHANGELOG_v1_to_v2.md |
Paper v2 changelog β new boundary notes |
SECURITY.md |
Security policy and reporting path |
docs/BUILD.md |
Full build matrix (Coq, Rust, Python) |