eulerScalarGap
The definition extracts a normalized stiffness scalar from Euler carrier data at a defect sensor location. It multiplies the bounded logarithmic derivative by the admissible radius and divides by the carrier amplitude. Researchers modeling the unified Riemann hypothesis cite this scalar when constructing T1-bounded proxies. The construction is a direct algebraic combination of the three carrier quantities.
claimFor a defect sensor with real part $σ_0$, the normalized Euler stiffness parameter is $M_C(σ_0) · (σ_0 - 1/2) / C(σ_0)$, where $M_C$ is the carrier log-derivative bound, $C$ is the carrier amplitude, and $(σ_0 - 1/2)$ is the admissible radius to the critical line.
background
The Unified RH module organizes a three-component architecture that separates cost divergence from Euler trace admissibility to guarantee T1-bounded realizable ledgers. A DefectSensor is the structure that records the multiplicity (charge) and real part of a hypothetical zeta zero lying in the right half of the critical strip. carrierDerivBound supplies an upper bound on the logarithmic derivative of the Euler carrier, carrierValue its amplitude, and the radius term the distance from $σ_0$ to the line Re(s) = 1/2.
proof idea
The definition is a direct algebraic expression that multiplies the carrier derivative bound by the admissible radius and divides by the carrier value. It is a one-line wrapper over the three upstream carrier functions.
why it matters in Recognition Science
This scalar supplies the input to eulerScalarProxy and the theorems establishing uniform T1 defect bounds and positivity for the resulting proxies. It completes the packaging step inside the T1-Bounded Realizability Architecture, bridging Euler trace admissibility to the law of existence. In the Recognition Science chain it supports the transition from proved carrier properties to boundary-transport constraints without violating T1.
scope and limits
- Does not prove the scalar is positive.
- Does not bound annular cost.
- Does not establish carrier convergence.
- Does not apply outside Euler carriers.
formal statement (Lean)
150noncomputable def eulerScalarGap (sensor : DefectSensor) : ℝ :=
proof body
Definition body.
151 carrierDerivBound sensor.realPart * eulerCarrierRadius sensor /
152 carrierValue sensor.realPart
153
154/-- The normalized Euler stiffness parameter is strictly positive. -/