reciprocal_primeEulerEvent_mem_sensorEulerLedger_of_subset
plain-language theorem explainer
The theorem establishes that reciprocal prime Euler events remain in the sensor Euler ledger events when the prime support enlarges from S to any T containing S. Researchers constructing directed families of finite arithmetic ledgers cite it to secure coherence under inclusion. The proof is a one-line wrapper applying the base membership lemma to the subset hypothesis.
Claim. Let $Ssubseteq T$ be finite prime supports. For a defect sensor and prime $p in S$, the reciprocal of the prime Euler event for $p$ belongs to the events of the Euler ledger attached to the sensor over support $T$.
background
PrimeSupport is the type of finite sets of primes indexing stages of concrete Euler ledgers. The sensorEulerLedger constructs, for each such support, a ledger whose events include prime Euler events generated from the sensor's real part together with their reciprocals under the LedgerForcing operation. Upstream, reciprocal from LedgerForcing inverts source and target of a recognition event while preserving the positive ratio; the base membership lemma reciprocal_primeEulerEvent_mem_sensorEulerLedger already places the reciprocal inside the ledger for the original support.
proof idea
The proof is a one-line wrapper that applies the lemma reciprocal_primeEulerEvent_mem_sensorEulerLedger to the given sensor and the image of p under the subset inclusion hST.
why it matters
The result supplies the coherence property required to define the canonical directed concrete Euler-ledger system in concreteDirectedEulerLedgerSystem. It completes the directed-family construction described in the module documentation, which packages finite arithmetic ledgers and connects them to ontology interfaces while leaving open the global physical-identification step to RSPhysicalThesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.