RecognitionThetaGeometricMajorant
plain-language theorem explainer
RecognitionThetaGeometricMajorant encodes a reusable sufficient condition for summability of the recognition theta terms via domination by a geometric sequence. Researchers working on convergence of the Recognition Theta series cite this structure to discharge sub-conjecture A.1. The declaration is a plain structure definition that packages nonnegative constants C and q with q less than 1 together with the uniform norm bound on the terms.
Claim. A geometric majorant consists of real numbers $C$ and $q$ satisfying $C ≥ 0$, $0 ≤ q < 1$, such that for every $t > 0$ and every natural number $n$ the norm of the recognition theta term at parameters $t$ and $n$ is at most $C q^n$.
background
Recognition theta terms appear in the series expansion of the recognition function under the Recognition Composition Law. The module tracks sub-conjecture A.1, which requires summability of these terms for every positive $t$. A geometric majorant supplies a summable nonnegative upper bound of the form $C q^n$ with $q < 1$ that is independent of $t$ after the first term.
proof idea
This is a structure definition with no computational content. It directly records the constants $C$ and $q$, their nonnegativity and strict upper bound on $q$, and the term-norm inequality without any reduction or tactic steps.
why it matters
The structure feeds majorant_of_geometric and recognitionThetaConvergence_of_geometricMajorant, which together discharge the comparison step inside RecognitionThetaConvergenceAttackSurface. It supplies the concrete input needed to prove A.1 once a geometric bound is exhibited, closing the path from term estimates to full summability in the Recognition Science number-theory development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.