# Tokitai Documentation
A guided index to every `.md` file under `docs/`. The docs are
grouped by topic; start with **Architecture and navigation** below
for a high-level map, then jump into the bucket that matches what
you are working on.
## Architecture and Navigation
- [`module_index.md`](module_index.md) — 1-line per source file
across `src/`; the canonical "where is X implemented" pointer.
- [`release_gates_summary.md`](release_gates_summary.md) — which
tests gate which paper claims; the read-this-before-touching-
claims code map.
- [`release_progress.md`](release_progress.md) — phase-by-phase
status of the release roadmap; pairs with `todo.json`.
- [`dev/architecture_diagrams.md`](dev/architecture_diagrams.md) —
hand-curated Mermaid diagrams for the 8-layer architecture,
planner pipeline, proof-replay trace flow, and theory-evidence
chain.
- [`development/local_dev_setup.md`](development/local_dev_setup.md) —
how to build, run all tests, run a single test, regenerate paper
artifacts.
- [`development/ci_debugging.md`](development/ci_debugging.md) —
how to read a failed GitHub Actions run and map it back to a
local repro.
- [`development/whatsnew.md`](development/whatsnew.md) —
1-paragraph "what changed recently" pointer; complements
`CHANGELOG.md`.
## Operator and Backend Surface
- [`operators.md`](operators.md) — the public op registry, by
family (arithmetic, NN, shape, index, p-adic, sheaf).
- [`sheaf_operator_family.md`](sheaf_operator_family.md) — the
`Cover` + `FiniteSite` + `SectionTable` op family.
- [`device_memory_model.md`](device_memory_model.md) — how device
memory is represented across the cpu / hip / gpu backends.
- [`hardware_abstraction_boundary.md`](hardware_abstraction_boundary.md) —
the explicit boundary between hardware-specific code and the
portable planner/op/verify layers.
- [`public_nonstandard_api.md`](public_nonstandard_api.md) —
experimental, non-claim-boundary APIs (opt-in).
## Verifier and Release Gates
- [`observability.md`](observability.md) — the 3 observability
commands (claim status, submission readiness, fail-closed audit).
- [`semantic_conformance_report.md`](semantic_conformance_report.md) —
the cross-backend conformance report format.
- [`theory_support_matrix.md`](theory_support_matrix.md) — what the
generated support matrix is and how to read it.
- [`theory_contract_core.md`](theory_contract_core.md) — the core
theory-contract types and obligations.
- [`theory_specific_operator_hardening.md`](theory_specific_operator_hardening.md) —
per-op theory evidence and per-op hardening tests.
- [`theory_engineering_release_gate.md`](theory_engineering_release_gate.md) —
the engineering release-gate that consumes the theory evidence.
- [`certified_padic_gemm_release_gate.md`](certified_padic_gemm_release_gate.md) —
the certified-valuation-sparse p-adic GEMM release gate.
- [`certified_rewrite_lowering_contracts.md`](certified_rewrite_lowering_contracts.md) —
the rewrite-and-lowering contract surface.
- [`accelerated_pilot.md`](accelerated_pilot.md) — the accelerated
pilot gate (gates `production_speedup_claim_allowed`).
- [`cpu_oracle_conformance.md`](cpu_oracle_conformance.md) — CPU
oracle conformance test layout.
- [`cross_backend_conformance.md`](cross_backend_conformance.md) —
cross-backend conformance test layout.
- [`finite_sheaf_gluing_theorem.md`](finite_sheaf_gluing_theorem.md) —
the finite sheaf gluing theorem statement and proof sketch.
- [`padic_valuation_skip_theorem.md`](padic_valuation_skip_theorem.md) —
the p-adic valuation-skip theorem statement and proof sketch.
- [`valuation_stratified_padic_matmul_admission.md`](valuation_stratified_padic_matmul_admission.md) —
the valuation-stratified p-adic matmul admission gate.
- [`math_bound_audit_traces.md`](math_bound_audit_traces.md) — the
math-bound audit-trace format.
- [`theorem_binding_registry.md`](theorem_binding_registry.md) —
registry of theorem bindings to operator lowering rules.
- [`first_of_kind_novelty_evidence.md`](first_of_kind_novelty_evidence.md) —
novelty-evidence checklist (gates `sci_q2_claim_allowed`).
- [`prior_art_certified_valuation_sparse_padic_gemm.md`](prior_art_certified_valuation_sparse_padic_gemm.md) —
prior-art survey for the certified valuation-sparse p-adic GEMM
claim.
- [`benchmark_application_evidence_matrix.md`](benchmark_application_evidence_matrix.md) —
benchmark application evidence matrix (gates
`production_speedup_claim_allowed`).
## Planner Internals
- [`padic_planner_resource.md`](padic_planner_resource.md) — the
p-adic planner's valuation-skip resource accounting.
- [`nonstandard_cost_model.md`](nonstandard_cost_model.md) — the
nonstandard cost model used by the planner for the certified
p-adic GEMM path.
- [`backend_lowering_cache.md`](backend_lowering_cache.md) — the
per-backend lowering cache, including its key-fingerprint
format.
## ROCm / HIP (gated behind `--features rocm-hip`)
- [`gpu_scaffold.md`](gpu_scaffold.md) — the GPU scaffold module
(lowering target, not yet an acceleration path).
- [`rocm_hip_dense_pilot.md`](rocm_hip_dense_pilot.md) — the dense
ROCm/HIP pilot (i32 add/mul/matmul).
- [`rocm_hip_hardware_contract.md`](rocm_hip_hardware_contract.md) —
the ROCm/HIP hardware contract (gates
`portable_rocm_claim_allowed`).
- [`rocm_hip_padic_valuation.md`](rocm_hip_padic_valuation.md) —
ROCm/HIP p-adic valuation-skip lowering (P290-P300 family).
- [`rocm_hip_padic_stratified_matmul.md`](rocm_hip_padic_stratified_matmul.md) —
ROCm/HIP valuation-stratified p-adic matmul.
- [`rocm_hip_proof_audit.md`](rocm_hip_proof_audit.md) — proof
audit for the ROCm/HIP lowering rules.
- [`rocm_hip_sheaf_locality.md`](rocm_hip_sheaf_locality.md) —
ROCm/HIP sheaf-locality lowering.
- [`rocm_padic_stratified_benchmarks.md`](rocm_padic_stratified_benchmarks.md) —
ROCm p-adic stratified benchmarks (raw).
- [`rocm_semantic_conformance_benchmarks.md`](rocm_semantic_conformance_benchmarks.md) —
ROCm semantic-conformance benchmarks.
- [`rocm_theory_optimization_paper_gate.md`](rocm_theory_optimization_paper_gate.md) —
ROCm theory-optimization paper gate.
## Schemas and Paper Artifacts
- [`schemas/`](schemas/) — JSON schemas for the support matrix,
audit report, benchmark reports, and the novelty-evidence
checklist.
- [`paper/`](paper/) — paper-section drafts and the canonical
"what does the artifact say" cross-reference.
- [`theorems/`](theorems/) — the theorem statements and the
Lean-side binding surfaces for each theorem package.
## How to Navigate This Tree
If you are a new contributor, read in this order:
1. [`../ARCHITECTURE.md`](../ARCHITECTURE.md) — 8-layer overview.
2. [`../ARTIFACT.md`](../ARTIFACT.md) — what the paper claims.
3. [`../CLAIMS.md`](../CLAIMS.md) — the 8 `*_claim_allowed` flags.
4. [`module_index.md`](module_index.md) — the source-tree map.
5. `observability.md` and `release_gates_summary.md` — how
claims are checked at runtime.
6. `operators.md` and the bucket for whatever you are working on
(verifier, planner, ROCm/HIP, etc.).