EulerLedgerOntologyInterface
plain-language theorem explainer
EulerLedgerOntologyInterface bundles a directed system of finite Euler ledgers over prime supports, an admissible Euler trace, and a T1-bounded realizability proxy for any given defect sensor. Researchers bridging arithmetic Euler data to physical ontology in Recognition Science would cite this packaging structure. It is assembled directly from the concrete directed system, the pre-established admissible trace, and the realizable proxy without additional proof steps.
Claim. For a defect sensor $s$, an Euler ledger ontology interface consists of a directed Euler ledger system $D(s)$ over prime supports, an admissible Euler trace $A(s)$, and a physically realizable ledger proxy $R(s)$.
background
The Directed Euler Ledger module organizes finite concrete Euler ledgers into directed systems indexed by prime supports. A DirectedEulerLedgerSystem for a sensor supplies a stage map from each PrimeSupport to a LedgerForcing.Ledger, together with proofs that every stage is balanced and every agent has zero net flow. The module then links this arithmetic package to ontology interfaces imported from UnifiedRH, supplying admissibility of the Euler trace and a T1-bounded realizability proxy.
proof idea
This is a structure definition that directly bundles three components: the directed ledger produced by concreteDirectedEulerLedgerSystem, the admissible trace from euler_trace_admissible, and the realizable proxy from euler_physically_realizable. No tactics or reductions are required; the declaration simply packages already-constructed objects into a single interface type.
why it matters
The structure supplies the input type for concreteEulerLedgerOntologyInterface_exists, the strongest currently proved bridge from arithmetic Euler data into the ontology layer. It fills the finite-to-directed arithmetic package described in the module documentation but leaves open the global physical-identification step that would transport the ledger into the PhysicallyExists predicate. In the Recognition framework it supports the connection between number-theoretic Euler ledgers and physical realizability without yet discharging RSPhysicalThesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.