Research-Stack/6-Documentation/docs/specs/break_glass_test_list.md

Break-Glass Test List

Validates the 4D × 2 fusion of fusions approach. Each test has: problem, expected dimension contribution, success criteria.

---

Dimension 1: Math (DeepSeek V4 Pro + Gemini 3.1 Pro)

T1.1 — Q16_16 positivity lemma

Problem: Prove that Q16_16 values are non-negative (a.val ≥ 0 for all a : Q16_16).
Expected: DeepSeek finds the Subtype proof; Gemini suggests omega.
Success: Lemma compiles, used by q16_merge_nz.

T1.2 — min(1, a+b) ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0

Problem: Prove q16_merge_nz for non-negative Q16_16.
Expected: DeepSeek structures the by_cases; Gemini finds the Q16_16.add_nonneg lemma.
Success: Theorem compiles, used by toPattern_merge.

T1.3 — boolMerge preserves gap (Fin 8 → Bool)

Problem: Prove boolMerge_preservesGap on Fin 8 → Bool.
Expected: Both models suggest native_decide or fin_cases.
Success: Theorem compiles with 0 sorry.

---

Dimension 2: Proof (Claude Opus + Cohere Command A+)

T2.1 — gap_factors via match + rfl

Problem: Prove verifySpectralGap = boolGap ∘ toPattern for 8-element lists.
Expected: Claude writes the match; Cohere structures the rfl chain.
Success: Theorem compiles with 0 sorry.

T2.2 — disjoint_factors via match + native_decide

Problem: Prove resonanceDegeneracy = 0 ↔ boolDisjoint for 8-element lists.
Expected: Claude writes the match; Cohere suggests native_decide after match.
Success: Theorem compiles with 0 sorry.

T2.3 — crossgap_factors via match + native_decide

Problem: Prove crossInputGap ↔ boolCrossGap for 8-element lists.
Expected: Same pattern as T2.2.
Success: Theorem compiles with 0 sorry.

---

Dimension 3: Code (GPT-5.5 + Kimi K2.6)

T3.1 — verifySpectralGap8 @[reducible] definition

Problem: Define a direct Bool expression for the gap check on 8 bins.
Expected: Kimi writes the definition; GPT finds the Spectrum.lean pattern.
Success: Definition compiles, verifySpectralGap_eq_8 proven by native_decide.

T3.2 — toPattern_merge proof

Problem: Prove toPattern (piecewiseMerge s e) = boolMerge (toPattern s) (toPattern e).
Expected: GPT suggests funext + fin_cases; Kimi writes the q16_merge_nz application.
Success: Theorem compiles with 0 sorry.

T3.3 — mergeCheck8_all extraction

Problem: Extract specific (s, e) pair from mergeCheck8_all.
Expected: GPT suggests List.all_get?; Kimi writes the range proof.
Success: Extraction compiles, gives mergeCheck8 ss ee = true.

---

Dimension 4: Diversity (GLM-5.2 + DeepSeek V4 Flash)

T4.1 — Boolean Quotient Lifting architecture

Problem: Design the Fin 8 → Bool as primary semantic domain.
Expected: GLM proposes the architecture; Flash validates it's correct.
Success: Architecture document with clean separation of concerns.

T4.2 — Rewrite ordering bug fix

Problem: Fix the line 338 rw [merge_bridge] failure.
Expected: Flash identifies the fix (add rw [gap_bridge] first).
Success: cleanMerge_preservesGap compiles with 0 sorry.

T4.3 — Counterexample search

Problem: Verify no counterexample exists to cleanMerge_preservesGap.
Expected: Flash confirms theorem is true; GLM suggests edge cases to check.
Success: Confirmed no counterexample.

---

Cross-Dimension Tests

T5.1 — Math + Proof: q16_merge_nz → toPattern_merge

Problem: Chain T1.2 (q16_merge_nz) into T2.1 (gap_factors) to close the merge bridge.
Expected: DeepSeek proves q16_merge_nz; Claude applies it in toPattern_merge.
Success: toPattern_merge compiles with 0 sorry.

T5.2 — Math + Code: boolMerge_preservesGap → mergeCheck8_all

Problem: Use T1.3 (boolMerge_preservesGap) to validate T3.3 (mergeCheck8_all extraction).
Expected: DeepSeek proves the boolean theorem; GPT extracts it into the Q16_16 proof.
Success: Extraction compiles, gives the final conclusion.

T5.3 — Proof + Code: factor theorems → main theorem

Problem: Chain T2.1-T2.3 (factor theorems) into T4.2 (main theorem fix).
Expected: Claude writes the factor theorems; Kimi chains them into the main proof.
Success: cleanMerge_preservesGap compiles with 0 sorry.

T5.4 — Full Fusion: all dimensions → closed sorry

Problem: Close the cleanMerge_preservesGap sorry using all 8 models' contributions.
Expected: Each dimension contributes one piece; synthesis chains them.
Success: Theorem compiles with 0 sorry. Build: 3314 jobs, 0 errors.

---

Execution Protocol

1. Single dimension: Run 2 models on their assigned tests. Cost: ~$0.20-0.50 per dimension.
2. Cross-dimension: Run the 2 relevant models on cross-dimension tests. Cost: ~$0.30-0.80 per test.
3. Full fusion: Run all 8 models on T5.4. Cost: ~$1.50-3.00.
4. Total: ~$5-10 for the complete test suite.

Success Criteria

Level	Criteria
Pass	All T1.x-T4.x tests pass (single dimension)
Pass+	All T5.x tests pass (cross-dimension)
Complete	T5.4 passes (sorry closed, build green)