finitePrimeLedgerPartition_insert_nonprime
plain-language theorem explainer
The finite prime-ledger partition remains unchanged when a non-prime natural number is inserted into its index set. Number theorists formalizing Euler products would cite this invariance to restrict attention to primes without loss of generality. The proof is a direct unfolding of the product definition followed by simplification on the non-membership and non-primality hypotheses.
Claim. Let $s$ be complex and $S$ a finite set of natural numbers. For $n$ not in $S$ and not prime, the product over $S$ union $n$ of the local factor (primeLedgerLocalPartition $s$ $p$ if $p$ prime, else 1) equals the product over $S$.
background
The Euler Ledger Partition module packages the Euler product as the partition function of independent prime-ledger postings. The finite prime-ledger partition is the product over a Finset of naturals, inserting the local factor only for primes and 1 otherwise. This isolates finite statements before the infinite equality with riemannZeta is handled in EulerLedgerPartitionCert.
proof idea
The proof is a one-line wrapper that unfolds finitePrimeLedgerPartition and applies simp using the non-membership and non-primality hypotheses.
why it matters
This invariance supports the finite product statements that precede the EulerLedgerPartitionCert. It ensures the partition function depends only on primes, aligning with the module's treatment of the Euler product as independent prime contributions. In the Recognition Science framework it is consistent with the packaging of constants and the J-function fixed point, though it touches no open question directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.