primePostingWeight
plain-language theorem explainer
primePostingWeight supplies the complex weight p to the power of negative s for each natural number p at scale s. It serves as the local factor in the decomposition of the Euler product into prime contributions within the Recognition Science ledger framework. Number theorists and formalizers of analytic number theory would cite this definition when building the product over primes. The definition is realized as a direct one-line complex exponentiation.
Claim. For a complex scale $s$ and natural number $p$, the prime posting weight is $p^{-s}$.
background
The Euler Ledger Partition module interprets the Euler product as the partition function generated by independent prime-ledger postings. This definition isolates the contribution of a single prime p scaled by s. It relies on the foundational definitions of the unit element in integers, rationals, and the phi-closed property from the core recognition specification.
proof idea
The definition is a direct abbreviation that equates primePostingWeight s p to the complex number obtained by raising p to the power -s. No additional lemmas or tactics are invoked beyond the built-in complex exponentiation.
why it matters
This definition provides the atomic weight used to construct the local partition factor (1 - weight)^{-1} at each prime, which assembles into the finite prime-ledger partitions and the structural certificate equating the Euler product to the Riemann zeta function. It fills the local geometric factor in the Recognition Science packaging of the zeta function as a ledger partition. The construction connects to the infinite product representation for Re(s) > 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.