pith. machine review for the scientific record. sign in
def definition def or abbrev high

concreteDirectedEulerLedgerSystem

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

Lean usage

def exampleInterface (s : DefectSensor) := concreteEulerLedgerOntologyInterface s

formal statement (Lean)

 101noncomputable def concreteDirectedEulerLedgerSystem (sensor : DefectSensor) :
 102    DirectedEulerLedgerSystem sensor where
 103  stage := sensorEulerLedger sensor

proof body

Definition body.

 104  stage_balanced := sensorEulerLedger_balanced sensor
 105  stage_net_flow_zero := sensorEulerLedger_net_flow_zero sensor
 106  stage_prime_pair := by
 107    intro support p hp
 108    exact ⟨primeEulerEvent_mem_sensorEulerLedger sensor hp,
 109      reciprocal_primeEulerEvent_mem_sensorEulerLedger sensor hp⟩
 110  stage_prime_pair_mono := by
 111    intro S T p hST hp
 112    exact ⟨primeEulerEvent_mem_sensorEulerLedger_of_subset sensor hST hp,
 113      reciprocal_primeEulerEvent_mem_sensorEulerLedger_of_subset sensor hST hp⟩
 114  directed_support := primeSupport_directed
 115  stage_cost_formula := sensorEulerLedger_cost_formula sensor
 116
 117/-- A convenient union-stage corollary: the union support contains the prime
 118data from both constituent supports. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.