sensorEulerLedger
sensorEulerLedger attaches a concrete LedgerForcing.Ledger to a defect sensor by feeding its real part as exponent into the finite Euler ledger builder over a given prime support. Researchers bridging arithmetic Euler products to double-entry recognition ledgers cite this as the explicit finite-support bridge object. The definition is a one-line wrapper that delegates to finiteEulerLedger after extracting the positive real part and converting the Finset to a list.
claimLet $S$ be a finite set of primes and let $L$ be a defect sensor whose real part satisfies $0 < L$. The sensor Euler ledger is the ledger obtained by starting from the empty ledger and successively adjoining, for each prime $p$ in $S$, the Euler event of ratio $p^{-L}$ together with its reciprocal.
background
The Concrete Euler Ledger module supplies the first arithmetic-to-ledger identification step. For any positive real exponent and any finite prime support it produces an actual LedgerForcing.Ledger whose recognition-event ratios are the Euler terms $p^{-σ}$ together with their reciprocals. A DefectSensor supplies the coordinate via its realPart field; the upstream sensor_realPart_pos fact guarantees positivity. The key upstream construction is finiteEulerLedger, which builds the ledger recursively: the empty list yields the empty ledger, and each prime is added via primeEulerEvent while preserving balance at every step.
proof idea
The definition is a one-line wrapper. It extracts the real part of the sensor, invokes the positivity witness sensor_realPart_pos, converts the Finset support to a list, and passes both to finiteEulerLedger.
why it matters in Recognition Science
This definition supplies the concrete object used by sensorEulerLedger_identification, which records balance, zero net flow, and explicit prime-event membership. It realizes the module's stated purpose of providing the first fully concrete bridge with double-entry balance by construction and an explicit total J-cost formula. In the Recognition framework it supplies the finite-support arithmetic example required before lifting to the Recognition Composition Law and the T0-T8 forcing chain.
scope and limits
- Does not extend to infinite prime supports.
- Does not derive the full physical thesis from the ledger alone.
- Does not compute numerical ledger costs for concrete sensors.
- Does not incorporate non-prime recognition events.
formal statement (Lean)
183noncomputable def sensorEulerLedger (sensor : DefectSensor) (support : Finset Nat.Primes) :
184 LedgerForcing.Ledger :=
proof body
Definition body.
185 finiteEulerLedger sensor.realPart (sensor_realPart_pos sensor) support.toList
186
187/-- The sensor-indexed concrete Euler ledger is balanced. -/
used by (9)
-
primeEulerEvent_mem_sensorEulerLedger -
reciprocal_primeEulerEvent_mem_sensorEulerLedger -
sensorEulerLedger_balanced -
sensorEulerLedger_cost_formula -
sensorEulerLedger_identification -
sensorEulerLedger_net_flow_zero -
concreteDirectedEulerLedgerSystem -
primeEulerEvent_mem_sensorEulerLedger_of_subset -
reciprocal_primeEulerEvent_mem_sensorEulerLedger_of_subset