recognitionThetaConvergence_of_majorant
plain-language theorem explainer
A majorant package establishes absolute convergence of the Recognition Theta series for every positive time. Researchers working on sub-conjecture A.1 would cite this comparison result to reduce the summability question to the existence of a dominating summable sequence. The proof is a direct application of the norm-bounded summability lemma to the supplied majorant bounds.
Claim. If a nonnegative majorant function $M(t,n)$ satisfies that for every $t>0$ the series $M(t)$ is summable and $|$recognitionThetaTerm$(t,n)|$ is bounded by $M(t,n)$ for all $n$, then the series of recognitionThetaTerm$(t,n)$ converges absolutely for every $t>0$.
background
RecognitionThetaConvergence is the structure stating sub-conjecture A.1: the series of recognitionThetaTerm $t$ $n$ is summable for each $t>0$. RecognitionThetaMajorant packages a majorant function together with its summability for each positive $t$ and the pointwise norm bound on the terms. The module tracks sub-conjecture A.1 and supplies the general comparison theorem needed to discharge it from lower bounds on costSpectrumValue and upper bounds on phi-rung weights.
proof idea
The proof is a one-line wrapper that applies the of_norm_bounded lemma to the summable_majorant and term_norm_le fields of the supplied RecognitionThetaMajorant.
why it matters
This theorem supplies the general comparison principle needed to discharge sub-conjecture A.1. It is invoked by the attack surface definition and by the geometric majorant specialization. In the broader framework it closes the gap between the abstract summability requirement and explicit bounds derived from costSpectrumValue and phi-rung weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.