pith. machine review for the scientific record. sign in
theorem proved term proof high

sensor_realPart_pos

show as:
view Lean formalization →

The real part of any defect sensor is strictly positive by the right-half critical-strip placement of its zero. Researchers constructing arithmetic ledgers from Euler factors cite this to guarantee that the exponents yield positive real ratios less than one. The proof is a one-line linear-arithmetic discharge of the first component of the sensor's in-strip hypothesis.

claimLet $s$ be a defect sensor whose associated zero of the reciprocal zeta function lies in the right half of the critical strip. Then the real part of $s$ satisfies $0 < s$.

background

A defect sensor is a structure recording an integer charge (the multiplicity of a zero of zeta) together with a real number that is the real part of that zero location; the in-strip predicate asserts that this real part lies strictly between 0 and 1. The Concrete Euler Ledger module builds a finite LedgerForcing ledger whose recognition events are the Euler factors $p^{-s}$ and their reciprocals, indexed by the same real part $s$ taken from the sensor. This supplies the first fully concrete arithmetic object that is balanced by construction and has zero net flow.

proof idea

The proof is a one-line term that applies linear arithmetic to the first projection of the in-strip field carried by the input sensor.

why it matters in Recognition Science

The result is invoked by sensorEulerLedger and by the membership theorems that place prime Euler events inside the sensor-indexed ledger; it thereby feeds the identification theorem establishing balance, zero net flow, and an explicit total J-cost formula. In the Recognition framework it ensures the exponents remain positive, so that each prime event carries a positive J-cost consistent with the forcing chain from T5 (J-uniqueness) onward.

scope and limits

formal statement (Lean)

  35theorem sensor_realPart_pos (sensor : DefectSensor) : 0 < sensor.realPart := by

proof body

Term-mode proof.

  36  linarith [sensor.in_strip.1]
  37
  38/-- The basic arithmetic recognition event contributed by a prime Euler factor.
  39
  40Its ratio is the positive real quantity `p^{-σ}`. -/

used by (11)

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

depends on (5)

Lean names referenced from this declaration's body.