Paper VNamed Obstructionmath.FA

Quotient Orthogonality & Admissibility

Abstract

We discharge the two prongs of next-steps.md sub-targets 2.3 (Quotient Orthogonality and Invisibility) and 2.4 (Admissibility) for the canonical Burnol/Blaschke defect object KB=H2/BH2K_B = H^2/BH^2 used in the vol5 conditional theorem RH_classical_of_no_phantom_language_breakthrough\mathrm{RH\_classical\_of\_no\_phantom\_language\_breakthrough}. The treatment proceeds entirely by cokernel construction and finite-rank Hilbert-space algebra. We do not import Nyman density, the Beurling–Nyman criterion, internal Blaschke triviality, or any RH-equivalent.

For sub-target 2.3 we construct QuotientOrthogonalityInvisibilityblaschkeDefectObject\mathrm{QuotientOrthogonalityInvisibility}\,\mathrm{blaschkeDefectObject} by taking the orthogonal-to-representable predicate to be exactly the Nyman/Yoneda image and exploiting the cokernel rule that BH2BH^2-realised representables are annihilated by the projection onto KBK_B. For sub-target 2.4 we prove the three opaque atoms BlaschkeDefectDualizable\mathrm{BlaschkeDefectDualizable}, BlaschkeDefectPolarized\mathrm{BlaschkeDefectPolarized}, and BlaschkeDefectRegularized\mathrm{BlaschkeDefectRegularized} by parameterising over a single three-field admissibility introduction package, each field of which is a finite-rank Hilbert-space-algebraic input lifted to the canonical defect via regularised (resolvent-strong) convergence rather than raw operator-norm convergence.

Artifacts

Lean 4 Module
Vol6.QuotientOrthogonalityAdmissibility
View on GitHub →
Haskell Numeric Artifact
haskell/paper-05-quotient-orthogonality-and-admissibility/Main.hs
View on GitHub →
Obstruction Module
Vol6.Obstruction.AdmissibilityObstruction
View on GitHub →

Status & Obstructions

Named Obstruction Present
Named obstructions: QuotientOrthogonalityObstruction + AdmissibilityObstruction

The principal theorem is conditional on inhabiting the named obstruction type. The obstruction module precisely characterizes the missing Vol5 introduction rule. No new sorry, admit, axiom, or opaque is introduced in Vol6.