concreteDirectedEulerLedgerSystem
plain-language theorem explainer
The definition assembles the canonical directed Euler ledger system for any DefectSensor by setting its stage to sensorEulerLedger and populating the remaining structure fields from sensor-specific lemmas. Number theorists bridging concrete arithmetic ledgers to the Recognition ontology would cite this construction to obtain a ready-to-use DirectedEulerLedgerSystem instance. The proof is a direct noncomputable structure definition that invokes balanced, net-flow, prime-pair, and cost lemmas for each field.
Claim. For a defect sensor $s$, the concrete directed Euler ledger system is the structure whose stage at each prime support $S$ is the ledger produced by sensorEulerLedger($s$), every stage is balanced with zero net flow, every prime in the support contributes both its Euler event and reciprocal, the assignment is monotonic under support enlargement, the support is directed, and the cost formula holds.
background
DirectedEulerLedgerSystem is the structure (defined in the same module) that packages a family of concrete Euler ledgers indexed by PrimeSupport, requiring stage : PrimeSupport → LedgerForcing.Ledger together with proofs that every stage is balanced, has zero net flow for every agent, supplies both Euler event and reciprocal for each prime, is monotonic under inclusion, and obeys the cost formula. The module packages finite concrete Euler ledgers from ConcreteEulerLedger into a directed system over finite prime supports and links them to the ontology interfaces in UnifiedRH. Upstream lemmas such as primeEulerEvent_mem_sensorEulerLedger and sensorEulerLedger_balanced supply the concrete arithmetic facts used to discharge the structure fields.
proof idea
The definition is a direct structure constructor. It sets stage to sensorEulerLedger sensor, then supplies stage_balanced and stage_net_flow_zero by direct application of the corresponding sensor lemmas, discharges stage_prime_pair and stage_prime_pair_mono by intro-exact on the primeEulerEvent_mem_sensorEulerLedger and reciprocal variants (including the subset forms), and fills directed_support and stage_cost_formula by the named lemmas primeSupport_directed and sensorEulerLedger_cost_formula.
why it matters
This definition supplies the concrete directed ledger instance that concreteEulerLedgerOntologyInterface consumes to produce the combined directed-ledger/admissible-trace/realizable-proxy package. It thereby completes the finite-support arithmetic side of the Euler ledger ontology interface described in the module documentation, while the remaining global physical-identification step to PhysicallyExists (via eulerLedgerScalarState rather than the bounded proxy) is left open. The construction sits inside the number-theory bridge that prepares the Recognition Science ledger for later unification with the forcing chain and physical thesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.