primeSupport_directed
plain-language theorem explainer
Finite sets of primes are directed under inclusion. Researchers constructing directed systems of concrete Euler ledgers cite this to guarantee any two finite prime supports admit a common upper bound. The proof is a one-line wrapper that exhibits the union and invokes the standard Finset subset lemmas.
Claim. For any two finite sets of primes $S$ and $T$, there exists a finite set of primes $U$ such that $Ssubseteq U$ and $Tsubseteq U$.
background
The module packages finite concrete Euler ledgers from ConcreteEulerLedger into a directed system indexed by finite prime supports, then links the system to ontology interfaces in UnifiedRH. PrimeSupport is the abbreviation Finset Nat.Primes that indexes the stages of these concrete ledgers. The local setting requires coherence under support enlargement: every prime present in a smaller support remains present after enlargement.
proof idea
The proof is a one-line wrapper that applies the exact tactic to the pair consisting of the union S ∪ T together with the two standard lemmas Finset.subset_union_left and Finset.subset_union_right.
why it matters
This result supplies the directedness axiom needed by the downstream definition concreteDirectedEulerLedgerSystem. It completes the coherence-under-enlargement step listed in the module documentation for the Directed Euler Ledger Interface, thereby supporting the admissible Euler trace and T1-bounded proxy already established upstream. The declaration does not yet close the remaining gap to RSPhysicalThesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.