warrantable: machine-checked capability governance and elevation provenance (Verus proof artifact)

A Verus proof artifact for capability-gated authorization. Verified at commit3d80ce25f9aef5cf64a91ac6c88087ee05ecff77: 20 verified, 0 errors, 0 admits,0 assumes, under Verus 0.2026.06.07.cd03505 with Z3 4.12.5.WHAT IS ESTABLISHED. thm_no_bypass proves that in any reachable state, everycapability in `issued` bears the tag governance would have computed under itsepoch key, discharged by state-machine induction with govern_issue as the solewriter of `issued`. thm_elev_governance_provenance proves that every elevationin `elev` is backed by a governance-minted capability at that tier. Theinherited escalation_theorem is retained unchanged and is definitional givenmay_influence; it is carried for continuity, not for strength, and is disclosedas such in its docstring. Neither theorem should be quoted without itscounterexample results.WHAT THE RESULTS REST ON. The results are structural over an uninterpreted MAC.k_gov and mac are the only uninterpreted functions in the crate, and mac carriesno algebraic properties by design: not injectivity, not collision resistance,not one-wayness. There is no assume, no admit, no external_body and no#[verifier::] escape hatch anywhere.ASSUMPTIONS OF RECORD (prose, not Verus constructs, and a different quantityfrom ASSUMED: 0). A1, MAC unforgeability (EUF-CMA), irreducible in Verus, whichhas no notion of computational hardness; unforgeability is assumed of eachk_gov(e) separately, and thm_retired_epoch_rejected bounds what one leaked epochkey buys. A2-residual, demux correspondence: the model contains noband-from-payload path, but that ingest's channel argument corresponds to thephysical arrival channel is a fact about the implementation, guarded by testsrather than by any theorem here.NON-VACUITY. Six negative artifacts accompany the proofs and every one isconfirmed rejected. A verified count is not evidence of content:minted_by_governance once returned true, which made inv_nobypass constrainnothing and gave thm_no_bypass a postcondition of true, while Verus verifiedclean throughout. The detector is demonstrated to fire: stubbingelev_backed_by_governance to true makes ce6_elev_provenance_without_reachabilityverify and the suite raise its alarm at 5/6; with the real predicate it iscorrectly rejected at 6/6.REPRODUCTION. Run ./verify.sh and ./check_counterexamples.sh. The toolchain isnot vendored; README.md pins the exact version with a fetch recipe. Cold-startcost is a 26 MB download and nothing else: no build, no dependency resolution.PROVENANCE. warrantable supersedes auth_gate_th, which supersedes gdc_e_l2_th.Both are retained for history with supersession notices; neither was everdeposited.Archive SHA-256:84f19ba37a2b25c5932b6b0a3369e90651262f2841aae49e02e0f6917ee68354