recognitionThetaTerm
plain-language theorem explainer
The n-th term of the Recognition Theta function is defined as χ₈(n) ⋅ φ^{-r(n)} ⋅ exp(−t ⋅ c(n)), where r(n) is the phi-rung index and c(n) the cost spectrum value. Researchers constructing modular theta series in Recognition Science cite this as the elementary summand that folds in the 8-tick character and phi-ladder weight. The definition is a direct algebraic product with no lemmas or tactics.
Claim. The n-th term of the Recognition Theta function is given by $χ_8(n) ⋅ φ^{-r(n)} ⋅ exp(−t ⋅ c(n))$, where $r(n)$ is the phi-rung index of $n$ and $c(n)$ is the cost spectrum value of $n$.
background
The Recognition Theta function Θ̃_RS(t) is defined as the candidate completion of the ordinary cost theta series Θ_J(t) = Σ exp(−t c(n)) by multiplying each term by the 8-tick character χ₈ (from T7) and the phi-ladder weight φ^{-r(n)} (from T6). This construction is intended to support a modular identity under t ↦ 1/t, though that identity is stated only as a hypothesis structure in the module. The local setting is given by the module documentation: the series inherits its form from the Recognition Composition Law and the eight-tick octave while remaining elementary arithmetic.
proof idea
This is a direct definition: the term is the product chi8 n * phi ^ (- phiRung n) * Real.exp (- t * costSpectrumValue n). No upstream lemmas are invoked; the expression simply assembles the character, the rung scaling from RSNativeUnits.phiRung, and the cost value from PrimeCostSpectrum.costSpectrumValue.
why it matters
The term is the summand inside recognitionTheta (the tsum) and is referenced by recognition_theta_certificate, RecognitionThetaConvergence, and the even/odd vanishing theorems. It supplies the concrete realization of the 8-tick character (T7) and phi-ladder weight (T6) inside the theta series, advancing the modular-identity program of Sub-conjecture A.2. The module documentation notes that the full modular identity still requires phi-ladder Poisson summation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.