concreteDirectedEulerLedgerSystem_union_contains
plain-language theorem explainer
The declaration shows that the concrete directed Euler ledger system is monotonic under union of prime supports: any prime Euler event from a support in the union appears in the combined stage, along with its reciprocal. Number theorists building directed systems over primes in the Recognition framework cite this for coherence properties. The proof uses case split on the membership hypothesis followed by direct application of the stage monotonicity lemma.
Claim. Let $σ$ denote the real part of a defect sensor. For finite prime supports $S$ and $T$, and a prime $p$ belonging to $S$ or to $T$, the prime Euler event with ratio $p^{-σ}$ and its reciprocal both belong to the set of events in the stage indexed by $S ∪ T$ of the concrete directed Euler ledger system constructed from the sensor.
background
PrimeSupport is the type of finite sets of primes, serving as indices for stages in the directed Euler ledger system. The module constructs, for each defect sensor, a family of concrete finite arithmetic ledgers indexed by these supports, with coherence under enlargement: primes in smaller supports remain in larger ones. Upstream, primeEulerEvent defines the basic recognition event for a prime p with positive real part sigma, having ratio p to the power -sigma. The reciprocal operation from LedgerForcing inverts the source and target while taking the inverse ratio.
proof idea
The proof begins by defining the system from the sensor. It performs case analysis on whether p belongs to S or to T. In each case it invokes the stage monotonicity lemma of the system, supplying the appropriate subset inclusion (left or right union) and the membership hypothesis.
why it matters
This corollary supports the coherence of the directed family under support enlargement, as required for the finite-to-directed arithmetic package. It contributes to the admissible Euler trace and T1-bounded realizability proxy mentioned in the module. In the broader framework it advances the connection between concrete number-theoretic ledgers and the ontology interfaces, though the physical identification gap remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.