Z_RS_partial
plain-language theorem explainer
The declaration defines the N-term partial sum of the RS partition function as the finite sum of exp(-s J(phi^k)) terms. Mathematicians bridging the Langlands program to recognition cost would cite this as the concrete starting point for L-function approximations in the RS setting. The definition is a direct unfolding of the sum over the first N powers of the self-similar fixed point phi.
Claim. The N-term partial sum of the recognition partition function is given by $Z_{RS}(s,N) := sum_{k=0}^{N-1} exp(-s · J(φ^k))$, where $J$ denotes the recognition cost function and $φ$ the golden ratio fixed point.
background
In the Recognition Science framework the partition function Z_RS(s) arises as the sum over recognition costs J at successive phi-ladder rungs. The J-cost function satisfies the Recognition Composition Law and is defined via the forcing chain as J(x) = (x + 1/x)/2 - 1. This module opens the Langlands correspondence by identifying L-functions with such partition functions on the recognition Hilbert space.
proof idea
This is a direct definition that unfolds the partial sum using summation over the finite range of natural numbers up to N, with each term the exponential of minus s times the J-cost at phi to the power k.
why it matters
This definition supplies the finite approximant used in LanglandsCert to establish positivity of terms and in LanglandsRSBridge to state the structural correspondence between automorphic representations and recognition partitions. It fills the opening step in the RS framing of the Langlands program, where the full correspondence reduces to classifying representations of the recognition symmetry group. The module notes that the functional equation of any RS-compatible L-function holds by J-cost symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.