sensorEulerLedger_net_flow_zero
Zero net flow holds at every agent for the ledger built from a defect sensor's real part and finite prime support. Researchers closing the arithmetic-to-ledger bridge in Recognition Science cite this when verifying conservation for concrete Euler data. The proof is a one-line wrapper that unfolds the sensor definition and invokes the finite Euler ledger conservation theorem.
claimLet $L$ be the ledger whose events are the Euler factors $p^{-σ}$ (and reciprocals) for each prime $p$ in a finite support, where $σ$ is the positive real part of a defect sensor. Then the net flow of $L$ at any agent is zero.
background
The Concrete Euler Ledger module constructs explicit LedgerForcing.Ledger objects from prime Euler data. A DefectSensor is a structure holding the multiplicity of a zeta zero, its real part $σ > 0$ (enforced by sensor_realPart_pos via the in_strip hypothesis), and the strip location. The definition sensorEulerLedger attaches the finite list of primes to finiteEulerLedger at exactly this $σ$, producing a balanced double-entry ledger whose event ratios are the $p^{-σ}$ terms. Net flow at an agent is the sum of log(ratio) over events that touch the agent. The upstream theorem finiteEulerLedger_net_flow_zero states that every such finite Euler ledger has zero net flow at every agent, reducing to conservation_from_balance on the balanced ledger.
proof idea
The term proof unfolds sensorEulerLedger to obtain finiteEulerLedger at sensor.realPart (with the positivity hypothesis from sensor_realPart_pos), then applies finiteEulerLedger_net_flow_zero directly to the support list and agent.
why it matters in Recognition Science
This supplies the zero net flow clause required by the identification theorem sensorEulerLedger_identification (which packages balance, zero flow, and prime membership) and by concreteDirectedEulerLedgerSystem (which installs it as the stage property). It completes the first concrete arithmetic ledger bridge in the module, confirming conservation as an instance of the generic LedgerForcing conservation theorem. The result sits inside the T0-T8 forcing chain by furnishing a balanced ledger object at the arithmetic level before physical constants or dimensions are introduced.
scope and limits
- Does not extend to infinite prime supports or address convergence.
- Does not compute the explicit total ledger cost in terms of J.
- Does not derive physical constants or spatial dimensions.
- Does not prove uniqueness of the sensor-to-ledger map.
Lean usage
example (sensor : DefectSensor) (support : Finset Nat.Primes) (agent : ℕ) : LedgerForcing.net_flow (sensorEulerLedger sensor support) agent = 0 := sensorEulerLedger_net_flow_zero sensor support agentformal statement (Lean)
194theorem sensorEulerLedger_net_flow_zero (sensor : DefectSensor)
195 (support : Finset Nat.Primes) (agent : ℕ) :
196 LedgerForcing.net_flow (sensorEulerLedger sensor support) agent = 0 := by
proof body
Term-mode proof.
197 unfold sensorEulerLedger
198 exact finiteEulerLedger_net_flow_zero sensor.realPart (sensor_realPart_pos sensor) support.toList agent
199
200/-- Every supported prime contributes its Euler event to the sensor-indexed ledger. -/