sensorEulerLedger_net_flow_zero
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.