# FINAL SHEET — CUB-3x Verification Session, 2026-08-15 Source: branch `worktree-cub-3x-verify-2026-08-14` @ `be240d7eb37051829f7f77ebb257d27c6d7ff6a6`, PR #1394 (**unmerged** as of this writing) against `cubie-tf` origin/main `072e0dc76ba15bd5510cbf6cc1ce94e12b8aad42`. cubie-research side of the union generated from a clean `origin/main` checkout (`d6e2d7f21a5640b8...`), independent of any other in-progress local branch. Companion files (same 2026-08-15 batch): `unified_cub_registry_2026-08-15.json` (full 2597-row registry), `.csv` and `.jsonl` flattenings of the same data. This sheet embeds real, byte-accurate statement text (git-shown at the branch head, not paraphrased) for the theorems this session authored, re-anchored, or investigated; the CSV/JSON/JSONL carry pointers + full SHA-256 hashes for all 2597 rows including these. ## Task 4 — CubieBexarMetalV1_4Gap (10 new theorems) ### CUB-1636 — cub_1636_signal_le_crowd - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1636_signal_le_crowd : forall N, goldenPath N <= crowd N. ``` ### CUB-1637 — cub_1637_crowd_le_exposure - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1637_crowd_le_exposure : forall N, crowd N <= exposure N. ``` ### CUB-1638 — cub_1638_signal_to_exposure_gap - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1638_signal_to_exposure_gap : forall N, 10 ^ N * goldenPath N <= exposure N. ``` ### CUB-1639 — cub_1639_signal_to_crowd_gap - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1639_signal_to_crowd_gap : forall N, 5 ^ N * goldenPath N <= crowd N. ``` ### CUB-1640 — cub_1640_seam_exposed_ratio - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1640_seam_exposed_ratio : forall N, 9 * seamExposed N = 8 * 54 ^ (N + 1). ``` ### CUB-1641 — cub_1641_bounded_depth_bounds_exposure - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1641_bounded_depth_bounds_exposure : forall N Dmax, N <= Dmax -> exposure N <= exposure Dmax. ``` ### CUB-1644 — cub_1644_corner_consensus_weakest - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1644_corner_consensus_weakest : forall j1 j2 j3, cornerConsensus j1 j2 j3 = true -> j1 = true /\ j2 = true /\ j3 = true. ``` ### CUB-1645 — cub_1645_two_corner_decomposition - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1645_two_corner_decomposition : forall deploy gpu, writeOK deploy gpu = true <-> deploy = true /\ gpu = true. ``` ### CUB-1646 — cub_1646_corners_independent - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1646_corners_independent : writeOK true false = false /\ writeOK false true = false. ``` ### CUB-1656 — cub_1656_mul_pow_eq - Module: `CubieBexarMetalV1_4Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` ```coq Theorem cub_1656_mul_pow_eq : forall a b n, (a * b) ^ n = a ^ n * b ^ n. ``` ## Task 5 — CubieDriveMathV1_3Gap (6 new theorems) ### CUB-1657 — cub_1657_nesting_monotone - Module: `CubieDriveMathV1_3Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Gap.v`, `lean/CubieDriveMathV1_3Gap.lean`, `verus/cubie_drive_math_v1_3_gap_spec.rs` ```coq Theorem cub_1657_nesting_monotone : forall base K K', 1 <= base -> K <= K' -> coordChain base K <= coordChain base K'. ``` ### CUB-1659 — cub_1659_knill_laflamme_correctable - Module: `CubieDriveMathV1_3Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Gap.v`, `lean/CubieDriveMathV1_3Gap.lean`, `verus/cubie_drive_math_v1_3_gap_spec.rs` ```coq Theorem cub_1659_knill_laflamme_correctable : forall (L St : Type) (enc : L -> St) (err : St -> St), Recoverable enc err <-> InjectiveC (fun l => err (enc l)). ``` ### CUB-1664 — cub_1664_koopman_tracks_orbit - Module: `CubieDriveMathV1_3Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Gap.v`, `lean/CubieDriveMathV1_3Gap.lean`, `verus/cubie_drive_math_v1_3_gap_spec.rs` ```coq Theorem cub_1664_koopman_tracks_orbit : forall (St : Type) (phi : St -> St) (f : St -> nat) (n : nat) (x : St), koopman phi f n x = f (iterate phi n x). ``` ### CUB-1666 — cub_1666_bigraph_place_assoc - Module: `CubieDriveMathV1_3Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Gap.v`, `lean/CubieDriveMathV1_3Gap.lean`, `verus/cubie_drive_math_v1_3_gap_spec.rs` ```coq Theorem cub_1666_bigraph_place_assoc : forall h g f, composePlace (composePlace h g) f = composePlace h (composePlace g f). ``` ### CUB-1667 — cub_1667_judgmental_congruence - Module: `CubieDriveMathV1_3Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Gap.v`, `lean/CubieDriveMathV1_3Gap.lean`, `verus/cubie_drive_math_v1_3_gap_spec.rs` ```coq Theorem cub_1667_judgmental_congruence : forall (A B : Type) (f : A -> B) (a a' : A), a = a' -> f a = f a'. ``` ### CUB-1668 — cub_1668_judgmental_substitution - Module: `CubieDriveMathV1_3Gap` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Gap.v`, `lean/CubieDriveMathV1_3Gap.lean`, `verus/cubie_drive_math_v1_3_gap_spec.rs` ```coq Theorem cub_1668_judgmental_substitution : forall (A : Type) (P : A -> Prop) (a a' : A), a = a' -> P a -> P a'. ``` ## Task 8 — Ott fail-closed v2 (pre-existing Coq/Lean theorems; Verus coverage gap closed this session) CUB-3110/3112 below are the PRE-EXISTING theorems whose Verus pointer moved to the new v2 spec file this session. Task 8's own 4 newly-AUTHORED Verus theorems (gate_enforce_reachability, gate_enforce_load_bearing, gate_enforce_discriminates, present_invalid_not_verified) live under different CUB IDs not individually broken out here -- full pointers/hashes for every row, including those four, are in the CSV/JSONL export. ### CUB-3110 — no_spoof_only_valid_verifies - Module: `OttFailClosedVerification` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Lean verified-locally` Formal systems: `Coq+Lean` - Files: `coq/CUB_3110_3112_OttFailClosedVerification.v`, `lean/CUB_3110_3112_OttFailClosedVerification.lean`, `verus/CUB_3110_3112_OttFailClosedVerification_v2_spec.rs` _Statement (registry): SF-024 fail-closed OTT verification (SF #4)_ ### CUB-3112 — unverified_ott_denied_in_enforce - Module: `OttFailClosedVerification` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Lean verified-locally` Formal systems: `Coq+Lean` - Files: `coq/CUB_3110_3112_OttFailClosedVerification.v`, `lean/CUB_3110_3112_OttFailClosedVerification.lean`, `verus/CUB_3110_3112_OttFailClosedVerification_v2_spec.rs` _Statement (registry): SF-024 fail-closed OTT verification (SF #4)_ ## CUB-3064 — identity split from CUB-1656 (mul_pow_eq) ### CUB-3064 — denial_admit_iff_zero - Module: `v1_4_BexarMetalFormalization_0521` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Gap.v`, `lean/CubieBexarMetalV1_4Gap.lean`, `verus/cubie_bexar_metal_v1_4_gap_spec.rs` _Statement (registry): CUB integration: cubie-core_ ## Task 11 — CUB-1660 retagged (false triple-kernel credit removed) ### CUB-1660 — hypercontraction_decay - Module: `CubieDriveMathV1_3` Kind: `Theorem` Kernels: `none` - Status: `DRAFT` Formal systems: `Coq+Lean+Verus` - Files: `coq/v1_3_DriveMathFormalization_0521.v`, `lean/CubieDriveMathV1_3.lean` - Renamed identifier only; statement below is the CURRENT (post-fix) file, byte-identical in its proof obligation to the pre-fix stub. - This IS the real, untagged theorem CUB-1660's ID legitimately names (always existed at this file/line). It is NOT the content that used to carry the CUB-1660 tag: three separate stub files (coq/CUB_1660_GrgStep.v, lean/CUB_1660_GrgStep.lean, a verus proof fn) proved only the tautology step(seed)=step(seed) under a superseded 2021-roadmap misassignment, and were retagged off CUB-1660 this session (now coq/StepFnApplicationReflexive.v etc., commit 447b4c8e7). The real theorem is reproven, with Lean kernel-checked, under CUB-1713 below. Row still lists formal_systems=Coq+Lean+Verus, which overstates this row alone -- flagged, not fixed (owner decision). ```coq Theorem hypercontraction_decay : forall f w n, f <= w -> f ^ n <= w ^ n. ``` ## Task 2 — 22 Omega theorems registered (pre-existing proof content, newly catalogued) ### CUB-1679 — interface_count - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1680 — interface_dominates - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1681 — bexar_pow_le_pow_base - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1682 — witness_64_byte_atomic - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1683 — belnap_idem - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1684 — belnap_top_unit - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1685 — belnap_assoc - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1686 — vn_symmetry - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1687 — surface_spoofing_kill - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1688 — seam_requires_lineage - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1689 — goodput_no_overcommit - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1690 — ha_fail_closed - Module: `CubieBexarMetalV1_4Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieBexarMetalV1_4Omega.v`, `lean/CubieBexarMetalV1_4Omega.lean`, `verus/cubie_bexar_metal_v1_4_omega_spec.rs` _Statement (registry): Bexar Metal_ ### CUB-1709 — two_pow_pos - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1710 — n_lt_two_pow - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1711 — drive_pow_le_pow_base - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1712 — geometric_complexity_futility - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1713 — hypercontraction_decay - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1714 — fano_error_lower_bound - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1715 — kl_zero_leak_no_advantage - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1716 — topological_entropy_exponential - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1717 — power_law_monotone - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ### CUB-1718 — holevo_accessible_bounded - Module: `CubieDriveMathV1_3Omega` Kind: `Theorem` Kernels: `VCL` - Status: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` Formal systems: `Coq+Lean+Verus` - Files: `coq/CubieDriveMathV1_3Omega.v`, `lean/CubieDriveMathV1_3Omega.lean`, `verus/cubie_drive_math_v1_3_omega_spec.rs` _Statement (registry): Drive Math_ ## Task 10 — double-registration bands resolved (34 aliased, 5 ID collisions open) 39 CUB-30xx/CUB-16xx pairs were investigated (2026-07-02 bulk-import rows duplicating pre-existing legacy theorems). 34 were genuinely registry-only duplicates with no real artifacts of their own and were aliased CUB-30xx -> CUB-16xx in `roadmap/CUB_ALIAS_TABLE.csv` (additive, same mechanism as the pre-existing CUB-1669->CUB-3044 precedent). Full pair list: `docs/evidence/2026-08-15_cub_double_registration_summary.md`. **5 pairs (CUB-3046/3047/3048/3049/3050) are NOT double registrations -- they are genuine ID collisions needing an owner renumber decision.** Real, independently-authored artifacts exist under these IDs from 2026-07-07 (5 days after the bulk import claimed the same IDs for different theorems), so no alias direction is correct for any of the 5. **CUB-3048 is the sharp case: `deploy_today=true`, RUNTIME-INVOKED production code** (`cub_3048_gpa_to_shared_exec_binding` in `cubie-core/src/tdx_mem_wiring.rs:59`, traced through two independent call chains into `cubie-platform/src/admit_telemetry.rs`), while `roadmap/master_theorem_table.csv`'s CUB-3048 row claims VERIFIED/CANONICAL for an unrelated theorem (`judgmental_substitution`). **This needs an owner decision before the registry can state either meaning of CUB-3048 correctly.** ## Task 11 — a second, structurally identical instance found: CUB-1673 CUB-1660's false triple-kernel credit (three stub files proving only a tautology, tagged with an ID that belongs to a different, already-proven theorem) was fixed this session (see CUB-1660 above). The task's own investigation into how widespread this pattern is surfaced **CUB-1673 as a second, confirmed instance meeting the exact same criteria, NOT fixed (flagging only, matching how CUB-1660 itself was flagged before this session authorized fixing it):** - Registry theorem_name: `pow_le_pow_base` (`master_theorem_table.csv:1174`) - Real proof, untagged, in the same file CUB-1660's real proof lives in: `coq/v1_3_DriveMathFormalization_0521.v:20` - Already reproven under CUB-1711 (`CubieDriveMathV1_3Omega.v:16`, 0 axioms) - Its own artifacts (`coq/CUB_1673_ReservedStub.v`, `lean/CUB_1673_ReservedStub.lean`, `verus/CUB_1673_reserved_stub_spec.rs`) each discharge a bare `True`/`trivial`/empty-`ensures` tautology - `cub_audit.py` reports `kernels=VCL` for it, same false credit as CUB-1660 The wider pattern (files where EVERY theorem is a vacuous `True`-discharge, picked up by the audit's real text-or-filename CUB-ID matching rule, not just filename tags): **95 confirmed distinct IDs draw kernel credit solely from such files (117 on a looser bound), of which 11-14 are ALSO marked `deploy_today=true`** (CUB-1852, 1888, 1897, 1898, 1900, 1902, 1903, 1909, 1913, 1916, 1967 confirmed; 1208/1211/1860 on the looser measure). **This needs a scoping decision: extend the CUB-1660 remedy to this wider set, or leave it as a known, disclosed condition.** ## Report on triple-kernel-verified status (honest report, not a confirmation) Coq and Verus toolchains are NOT installed in this workspace (`docs/evidence/2026-08-14_cub_3x_toolchain_probe.md`) -- neither kernel ran even once this session. Every theorem this session touched or authored is labeled accordingly: `Coq PENDING-COQ-KERNEL; Verus PENDING-VERUS-KERNEL; Lean kernel-checked 4.30.0` -- never bare `VERIFIED` unless genuinely closed on all three kernels under that row's own ID. **"All triple-kernel verified" is not true of this branch's new content and is not claimed here.** What IS true, independently confirmed: - Every new/modified theorem's Lean leg was kernel-checked live this session (Lean 4.30.0, exit 0, axiom-free where claimed) -- not merely compiled, actually re-run and its `#print axioms` output captured. - Coq and Verus legs are closed proofs (no `Admitted`/`admit`/`sorry`/ `assume`) but UNVERIFIED BY A KERNEL in this environment -- honestly labeled PENDING, not claimed as passing. - 34 double-registration pairs resolved via alias (Task 10); 5 remain open ID collisions pending an owner renumber decision (CUB-3046-3050). - CUB-1660's false triple-kernel credit fixed; CUB-1673 (and a wider 95-117-ID pattern) found and flagged, not fixed, pending a scoping decision. Closing the Coq/Verus legs for real requires either installing those toolchains in this workspace or running the kernel-check on a machine that already has them -- out of scope for this session, noted here rather than worked around.