PrimeSupport
Finite sets of primes index the stages of concrete Euler ledgers attached to a defect sensor. Researchers constructing the directed system in the Recognition framework cite this abbreviation to parameterize the family of finite arithmetic ledgers over enlarging supports. The definition is a direct abbreviation of the Finset type over the set of primes, enabling union-based upper bounds.
claimLet $P$ be the set of prime numbers. The type of finite prime supports is the collection of all finite subsets of $P$, written as the Finset of $P$.
background
The Directed Euler Ledger Interface packages finite concrete Euler ledgers into a directed system over finite prime supports and connects them to ontology interfaces. The upstream Primes definition supplies the set of all primes as a subset of the naturals, with the prime sum converging for real exponents greater than 1. This supplies the indexing for stages where each finite support determines a ledger with balanced flows and zero net flow.
proof idea
This is a direct abbreviation of the Finset type constructor applied to the set of primes. No lemmas or tactics are invoked; the abbreviation simply identifies the indexing type used by the stage map in the directed system structure.
why it matters in Recognition Science
This abbreviation supplies the indexing set for the directed Euler ledger system, which feeds into theorems establishing concrete Euler ledger ontology interfaces with admissible traces and T1-bounded proxies. It advances the arithmetic-to-ontology bridge but leaves open the global physical-identification step that would transport the ledger into the PhysicallyExists predicate using the scalar state rather than the bounded proxy.
scope and limits
- Does not establish physical existence of the ledger beyond the bounded proxy.
- Does not discharge the global identification required for RSPhysicalThesis.
- Does not address analytic properties such as convergence of Euler sums over the supports.
formal statement (Lean)
38abbrev PrimeSupport := Finset Nat.Primes
proof body
Definition body.
39
40/-- Finite prime supports form a directed set under inclusion, with upper bound
41given by union. -/