feat(my-qtt): QTT verified-core checker — faithful Rust port of Coq R5/R5b

First strand of the fundamentals -> implementation coupling (the path the user
chose). proofs/STATUS.md flags that the mechanised QTT core and the Rust
compiler are 'two disconnected universes': checker.rs is a conventional Hindley
checker with no usage/multiplicity axis. This new crate ports the
machine-checked usage-walk synthesiser into the compiler's own language:

  - Q semiring {0,1,ω} (qadd/qmul/qle) — Coq Quantity.v tables verbatim
  - usage vectors (uzero/onehot/uadd/uscale/ule) — Coq SoloCore.v
  - check : Tctx -> Tm -> Option<(Ty,Uvec)> — the one-pass synthesiser
    (SoloCore.v:2128), returning the type AND exact realised usage
  - aff_check — the affine-budget decision (aff_type_dec / aff_type_iff, R5b)

Faithful de Bruijn (snoc-list <-> Vec, innermost = last). 7 tests green,
incl. the 4 SoloCore.v 'reflexivity' Examples reproduced as oracle tests
(check_id_unit / drop_linear / dup_linear / dup_omega) + the R5b affine
discard — so the port is checked against the verified algorithm's own
closed computations. No external deps; cargo test -p my-qtt passes.

Next coupling step: elaborate the my-lang surface AST onto this core so the
running checker enforces the resource axis. Refs proofs/STATUS.md.

Author: claude

Cargo.toml

@@ -5,6 +5,7 @@ members = [
     "crates/my-cli",   # Command-line interface (my binary)
     "crates/my-hir",
     "crates/my-mir",
+    "crates/my-qtt",   # QTT verified-core checker (faithful port of Coq R5 check / R5b aff_type_dec)
     "crates/my-llvm",  # LLVM code generation
     "crates/my-lsp",
     "crates/my-pkg",
@@ -33,6 +34,7 @@ repository = "https://github.com/hyperpolymath/my-lang"
 my-lang = { path = "crates/my-lang" }
 my-hir = { path = "crates/my-hir" }
 my-mir = { path = "crates/my-mir" }
+my-qtt = { path = "crates/my-qtt" }
 my-llvm = { path = "crates/my-llvm" }
 my-ai = { path = "crates/my-ai" }
 

crates/my-qtt/Cargo.toml

@@ -0,0 +1,12 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+[package]
+name = "my-qtt"
+version.workspace = true
+edition.workspace = true
+license.workspace = true
+authors.workspace = true
+repository.workspace = true
+description = "QTT verified-core checker for my-lang: a faithful Rust port of the machine-checked Coq usage-walk synthesiser (SoloCore.v R5 `check` / R5b `aff_type_dec`)."
+
+[dependencies]