# Theory-Engineering Release Gate
P206 adds `run_theory_engineering_release_gate`, a generated release gate for
the theory-engineered runtime boundary.
The gate checks:
- executable theory contracts for p-adic valuation, finite-site sheaf, and
categorical law witnesses
- theorem binding registry descriptors and checker transcripts
- semantic conformance report status, CPU oracle fixtures, and audit traces
- generated support-matrix rows for CPU support, GPU scaffold fallback, the
feature-gated dense-i64 pilot, the local ROCm/HIP hardware contract, and the
feature-gated real ROCm/HIP dense i32 pilot
- certified valuation-sparse p-adic GEMM claim evidence: dot/matrix theorem
bindings, dense CPU oracle, certified sparse CPU oracle, per-output
certificates, benchmark distribution coverage, HIP-or-fallback rows, and
speed-claim guards
- bounded optional Lean theorem-checker behavior: default timeout evidence is
recorded without blocking offline validation, while `TOKITAI_REQUIRE_LEAN=1`
remains fail-closed for missing, failing, or timed-out external Lean
execution
- public facade examples for p-adic planning/execution, finite-site sheaf
planning, prefer-GPU fallback, and strict-GPU rejection
- known limitation coverage and non-claim rows
The report exports stable JSON and Markdown. `cargo run --quiet --offline
--example paper_benchmarks` writes:
- `target/paper-results/theory-release-gate.json`
- `target/paper-results/theory-release-gate.md`
The gate is intentionally conservative. Passing it means the current runtime
boundary has executable contracts, theorem bindings, conformance evidence,
support rows, facade evidence, and documented limitations. It does not claim
full Rust formal verification, full p-adic algebra, general sheaf theory,
general category theory, broad GPU acceleration, or production performance.
The ROCm/HIP row records local hardware evidence only; passing this gate does
not imply HIP kernel execution.
The dense i32 ROCm/HIP pilot is a single feature-gated kernel with CPU-oracle
comparison, not a broad acceleration claim.
The certified p-adic GEMM row is fixed-precision and local-pilot evidence; it
does not claim full p-adic algebra, portable AMD GPU support, verified HIP
machine code, or production speedup. See
`docs/certified_padic_gemm_release_gate.md` for the P221 claim boundary.
The optional Lean timeout row is release reproducibility evidence only. It does
not turn the default gate into a full external proof-assistant verification
claim.
The required validation commands recorded by the gate are:
```bash
cargo fmt --check
python -m json.tool todo.json >/dev/null
cargo test --offline
cargo test --offline --features rocm-hip
cargo test --offline --features rocm-hip --test rocm_padic_stratified_benchmarks
cargo run --quiet --offline --example paper_benchmarks
cargo run --quiet --offline --features rocm-hip --example rocm_padic_stratified_benchmarks
sh scripts/check_padic_valuation_skip_theorem.sh
sh scripts/check_finite_sheaf_gluing_theorem.sh
TOKITAI_REQUIRE_LEAN=1 TOKITAI_LEAN_TIMEOUT_SECONDS=20 sh scripts/check_padic_valuation_skip_theorem.sh
TOKITAI_REQUIRE_LEAN=1 TOKITAI_LEAN_TIMEOUT_SECONDS=20 sh scripts/check_finite_sheaf_gluing_theorem.sh
```