primeEulerEvent_mem_sensorEulerLedger
plain-language theorem explainer
The membership theorem shows that for a defect sensor with positive real part σ and any finite prime support containing p, the recognition event of ratio p^{-σ} belongs to the events of the sensor-indexed Euler ledger. Number theorists building explicit arithmetic models of recognition processes cite this when verifying prime-event inclusion in concrete ledgers. The proof is a one-line wrapper that unfolds the sensor ledger definition and applies the list-membership lemma for finite Euler ledgers.
Claim. Let σ > 0 be the real part of a defect sensor. For any finite set S of primes containing p, the recognition event with source 0, target p and ratio p^{-σ} belongs to the events of the finite Euler ledger constructed from S at exponent σ.
background
The Concrete Euler Ledger module constructs an explicit LedgerForcing.Ledger from prime Euler data. A DefectSensor supplies the positive real part σ via sensor_realPart_pos. The primeEulerEvent for prime p at σ is the recognition event with ratio p^{-σ}. The sensorEulerLedger is defined as the finiteEulerLedger at that σ on the support list, which includes both each prime event and its reciprocal by the reciprocal definition in LedgerForcing.
proof idea
The proof unfolds sensorEulerLedger, reducing it directly to finiteEulerLedger applied to sensor.realPart and support.toList. It then applies the upstream theorem primeEulerEvent_mem_finiteEulerLedger, passing the membership hypothesis hp after a simpa conversion from Finset to List membership.
why it matters
This supplies the explicit prime-event membership step required by the downstream theorem sensorEulerLedger_identification, the first concrete arithmetic identification result asserting balance, zero net flow and prime-event membership. It feeds the construction of concreteDirectedEulerLedgerSystem and the subset-extension lemma. The result forms the initial arithmetic-to-ledger bridge object in the module before any full RSPhysicalThesis proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.