RecognitionThetaConvergenceAttackSurface
plain-language theorem explainer
The RecognitionThetaConvergenceAttackSurface structure packages the two comparison maps that turn a summable nonnegative majorant or a geometric majorant into absolute convergence of the Recognition Theta series for every t > 0. Researchers addressing sub-conjecture A.1 cite it to organize the remaining inputs required for summability. It is realized as a pure structure definition whose fields are supplied by the sibling comparison functions.
Claim. Let $M$ be a RecognitionThetaMajorant (a function $m(t,n)$ that is summable in $n$ for each $t>0$ and satisfies $||$recognitionThetaTerm $t n||$ $≤ m(t,n)$) and let $G$ be a RecognitionThetaGeometricMajorant (constants $C≥0$, $0≤q<1$ with $||$recognitionThetaTerm $t n||$ $≤ C q^n$). The structure supplies maps $M$ $↦$ RecognitionThetaConvergence and $G$ $↦$ RecognitionThetaConvergence, where RecognitionThetaConvergence asserts that the series of recognitionThetaTerm $t n$ is summable for every $t>0$.
background
The RecognitionTheta/Convergence module tracks sub-conjecture A.1, which requires absolute summability of the Recognition Theta series for all positive times. RecognitionThetaConvergence records precisely this summability statement. RecognitionThetaMajorant supplies a general summable nonnegative majorant together with the domination inequality, while RecognitionThetaGeometricMajorant specializes to geometric decay $C q^n$ with $q<1$; both are reusable sufficient conditions for the convergence claim. The upstream comparison theorem in the same module states that any such majorant immediately yields A.1.
proof idea
This is a structure definition with an empty body. It simply declares two fields whose values are the already-proved functions recognitionThetaConvergence_of_majorant and recognitionThetaConvergence_of_geometricMajorant. No tactics, reductions, or lemmas are applied inside the declaration itself.
why it matters
The structure organizes the attack surface for sub-conjecture A.1 by separating the proved comparison theorem from the remaining task of exhibiting a concrete majorant. It is instantiated directly by recognitionThetaConvergenceAttackSurface, which supplies the two comparison maps. The construction fills the general comparison step described in the module documentation and reduces the convergence question to bounds on costSpectrumValue and phi-rung weights. It leaves open the explicit construction of a geometric majorant after finitely many terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.