RecognitionThetaConvergence
plain-language theorem explainer
The Recognition Theta series, built from phi-rung weights and the mod-8 character, is asserted to converge absolutely for every t > 0. Number theorists and Recognition Science researchers modeling cost spectra would cite this as the basic convergence hypothesis needed before modular identities can be examined. The declaration is a one-field structure that packages the summability condition with no proof obligations.
Claim. Let $r(n)$ be the completely additive phi-rung index with $r(p) = ⌊log_φ p⌋$ for primes, and let $χ_8$ be the mod-8 character. Denote the n-th term of the Recognition Theta by $Θ̃_RS(t,n)$. Then the series $∑_n Θ̃_RS(t,n)$ is summable for every real $t > 0$.
background
The Recognition Theta $Θ̃_RS(t)$ completes the ordinary cost theta $Θ_J(t) = ∑ e^{-t c(n)}$ by weighting each term with the phi-ladder rung $r(n)$ and the eight-tick character $χ_8$. The rung function is completely additive, $r(mn) = r(m) + r(n)$, with the prime rule given in the sibling declarations phiRung_prime and phiRung_mul. The term recognitionThetaTerm(t,n) assembles the exponential decay, the rung power, and the character value into a single summand.
proof idea
This declaration is a structure definition that directly encodes the required summability predicate as a Prop; the proof body is empty. It functions as the target type for the majorant comparison theorems recognitionThetaConvergence_of_majorant and recognitionThetaConvergence_of_geometricMajorant in the same module.
why it matters
The structure states Sub-conjecture A.1 of the Recognition Science framework, the absolute convergence claim required before the modular identity (Sub-conjecture A.2) can be formulated. It is the immediate parent of the attack-surface structure and the two geometric-majorant theorems that discharge it. In the larger chain it supplies the analytic prerequisite for the eight-tick octave (T7) and the phi-ladder fixed point (T6) to produce a well-defined theta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.