recognitionThetaConvergence_of_geometricMajorant
plain-language theorem explainer
A geometric majorant on the Recognition Theta terms establishes their summability for every positive real t. Number theorists tracking sub-conjecture A.1 would cite this result to reduce the convergence question to the existence of a geometric bound. The proof is a one-line wrapper that converts the geometric structure to a general majorant and applies the comparison theorem.
Claim. Suppose there exist $C, q$ with $C, q$ nonnegative, $q < 1$, such that for all $t > 0$ and all $n$, the norm of the Recognition Theta term at $t, n$ is at most $C q^n$. Then the series of Recognition Theta terms converges for every $t > 0$.
background
This module tracks sub-conjecture A.1 on summability of Recognition Theta terms for every $t > 0$. RecognitionThetaGeometricMajorant is the structure that encodes a reusable sufficient condition: domination by a geometric sequence $C q^n$ with $q < 1$. The module proves the general comparison: any summable nonnegative majorant for each positive $t$ implies RecognitionThetaConvergence.
proof idea
The proof is a one-line wrapper that applies recognitionThetaConvergence_of_majorant to the output of majorant_of_geometric on the input geo.
why it matters
This theorem supplies the geometric case needed for recognitionThetaConvergenceAttackSurface, which records the current A.1 status via both the general and geometric comparisons. It advances the Recognition framework by showing how a geometric bound discharges the summability requirement in sub-conjecture A.1; the module states that the remaining content is the explicit construction of such a majorant from costSpectrumValue bounds and phi-rung weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.