spectral_correspondence_O3 (axiom)

/-- [III.T18] **CONJECTURE-AXIOM — CONDITIONAL RESULTS DOWNSTREAM** The O(3) spectral correspondence holds at all levels. This is one of exactly three conjecture-axioms in TauLib; see also `bridge_functor_exists` (`BookIII.Bridge.BridgeAxiom`) and `grand_grh_adelic` (`BookIII.Doors.GrandGRH`). **Conjectural scope.** At each finite level `k`, `spectral_correspondence_finite k` is decidable and verified computationally via `native_decide`. The axiom asserts that the finite correspondence extends to the universal statement `∀ k : Nat`. That extension is the conjectural content. **Mathematical content.** The spectral correspondence claims `ζ_τ(s) = 0 ⟺ Λ(s) ∈ Spec(H_L)`, with the determinant representation `ζ_τ(s) = det(I − Λ(s)·H_L⁻¹)`. This is the framework's honest conjectural gap in the τ-approach to RH. **Downstream theorems are CONDITIONAL RESULTS.** Any theorem whose transitive proof chain invokes `spectral_correspondence_O3` is conditional on the universal extension. Running `#print axioms ` on a downstream theorem will list `spectral_correspondence_O3`; readers should treat that theorem as a conditional result. **Preferred encoding (future work).** As with `bridge_functor_exists`, the Mathlib-community idiom would refactor downstream theorems to take this conjecture as an explicit hypothesis. Planned for a future wave. -/