majorant_of_geometric
plain-language theorem explainer
This definition converts a geometric majorant into the general majorant structure needed for Recognition Theta summability. Analysts checking sub-conjecture A.1 would cite it to reduce the series convergence question to a geometric bound. The construction is a direct record builder that inherits the term-norm inequality and invokes the standard geometric-series summability lemma.
Claim. Given constants $C, q$ with $C, q, C - q, 1 - q > 0$ such that the Recognition Theta term satisfies $||recognitionThetaTerm(t, n)|| ≤ C q^n$ for every $t > 0$, the function $M(t, n) := C q^n$ is a summable majorant: $M(t, ·)$ is summable for each fixed $t > 0$ and dominates the term norms.
background
RecognitionThetaMajorant packages a function $M : ℝ → ℕ → ℝ$ together with two properties: summability of $M(t, ·)$ for every $t > 0$ and the domination $||recognitionThetaTerm(t, n)|| ≤ M(t, n)$. RecognitionThetaGeometricMajorant is the special case in which $M(t, n) = C q^n$ with $0 ≤ q < 1$. The module Convergence tracks sub-conjecture A.1, which requires summability of the Recognition Theta series for every positive time; the comparison theorem in the same file shows that any summable majorant discharges A.1.
proof idea
One-line wrapper that builds the RecognitionThetaMajorant record by setting the majorant field to the geometric expression, delegating summability to Summable.mul_left applied to summable_geometric_of_lt_one, and copying the term-norm bound verbatim from the input geometric structure.
why it matters
It supplies the concrete bridge from the reusable geometric sufficient condition to the general majorant package used by recognitionThetaConvergence_of_geometricMajorant, which in turn proves RecognitionThetaConvergence and thereby discharges sub-conjecture A.1. The construction sits inside the Recognition Theta convergence argument that ultimately rests on lower bounds for costSpectrumValue and upper bounds on phi-rung weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.