RecognitionThetaMajorant
plain-language theorem explainer
RecognitionThetaMajorant packages a summable nonnegative function that bounds the absolute value of each Recognition Theta term for fixed positive t. Analysts proving summability of the Recognition Theta series cite this structure to invoke the comparison test. The declaration is a direct record of the majorant function together with its summability and termwise bound properties.
Claim. A structure consisting of a function $M : (0,∞) × ℕ → ℝ$ such that for every $t > 0$ the series $∑_n M(t,n)$ converges and $|χ_8(n) φ^{-φ-rung(n)} exp(-t · c(n))| ≤ M(t,n)$ for all $n$, where $c(n)$ denotes the cost-spectrum value at rung $n$.
background
The module tracks sub-conjecture A.1 on summability of the Recognition Theta series for every $t > 0$. The upstream definition recognitionThetaTerm supplies the explicit term $χ_8(n) φ^{-φ-rung(n)} exp(-t · costSpectrumValue n)$. The three upstream A constants record the active-edge count per fundamental tick and appear in the phi-power balance that fixes the rung weights.
proof idea
This is a structure definition that directly records the three fields: the majorant function, the summability assertion for each $t > 0$, and the termwise norm bound. No tactics or lemmas are applied inside the declaration itself.
why it matters
The structure supplies the hypothesis for the comparison theorem recognitionThetaConvergence_of_majorant that discharges sub-conjecture A.1. It is instantiated downstream by geometric majorants and appears in the RecognitionThetaConvergenceAttackSurface. The construction sits inside the Recognition Science forcing chain after the phi-ladder and cost spectrum have been fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.