primeEulerEvent_mem_sensorEulerLedger_of_subset
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the physical existence predicate for the ledger.
- Does not discharge the global RSPhysicalThesis.
- Does not address infinite supports or continuous limits.
- Does not derive new arithmetic identities beyond membership preservation.
formal statement (Lean)
47theorem primeEulerEvent_mem_sensorEulerLedger_of_subset
48 (sensor : DefectSensor) {S T : PrimeSupport}
49 (hST : S ⊆ T) {p : Nat.Primes} (hp : p ∈ S) :
50 primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
51 (sensorEulerLedger sensor T).events := by
proof body
Term-mode proof.
52 exact primeEulerEvent_mem_sensorEulerLedger sensor (hST hp)
53
54/-- Reciprocal prime-event membership also persists under support enlargement. -/