# 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) |