primeEulerEvent_mem_sensorEulerLedger_of_subset
plain-language theorem explainer
Prime-event membership in the sensor-indexed Euler ledger persists when the finite prime support enlarges. Researchers building directed systems of arithmetic ledgers cite this for coherence under inclusion. The argument is a one-line wrapper applying the base membership theorem to the image of the smaller support.
Claim. Let $S, T$ be finite sets of primes with $Ssubseteq T$ and let $p$ be a prime in $S$. For a defect sensor with positive real part $sigma$, the recognition event contributed by $p$ at ratio $p^{-sigma}$ belongs to the events of the Euler ledger attached to $T$.
background
PrimeSupport is the type of finite sets of primes, forming a directed set under inclusion with upper bounds given by union. The sensorEulerLedger attaches to each such support a concrete finite Euler ledger whose events are the primeEulerEvents for primes in the support, each carrying ratio $p^{-sigma}$ where $sigma$ is the sensor real part. The module packages these ledgers into a directed system over finite prime supports and records coherence under enlargement, as stated in the module doc: every prime already present in a smaller support remains present in any larger support.
proof idea
The proof is a one-line wrapper that applies the base theorem primeEulerEvent_mem_sensorEulerLedger to the membership of p in the smaller support S, using the inclusion hypothesis hST to obtain membership in T.
why it matters
This result supplies the coherence property required to construct the canonical directed concrete Euler-ledger system. It feeds directly into concreteDirectedEulerLedgerSystem. In the Recognition framework it completes the finite arithmetic stage of the directed Euler ledger before the remaining global physical-identification step that would transport the ledger into the PhysicallyExists predicate, which the module doc identifies as still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.