eulerCarrierRadius
plain-language theorem explainer
This definition computes the carrier-compatible radius for a defect sensor as its real part minus one half, giving the distance to the critical line Re(s) = 1/2. Researchers on the unified Riemann hypothesis architecture cite it when constructing the normalized stiffness parameter or proving T1 boundary behavior for realizable Euler ledgers. The implementation is a direct subtraction drawn from the sensor data.
Claim. For a defect sensor whose real part is denoted by σ, the carrier-compatible radius is σ - 1/2.
background
The Unified RH module organizes T1-bounded realizability around three components: cost divergence forced by nonzero charge, Euler trace admissibility proved from instantiation data, and physically realizable ledgers whose scalar proxy keeps the T1 defect uniformly bounded. A defect sensor marks a hypothetical location in the complex plane; its real part σ lies inside the critical strip. The module replaces an earlier claim of globally bounded annular cost with this structured ledger, relying on upstream carrier frequency definitions (5φ Hz) and compatibility notions from cellular automata and SAT backpropagation.
proof idea
The definition is a one-line arithmetic expression that subtracts 1/2 from the sensor's real part field.
why it matters
It supplies the admissible strip radius that feeds the positivity theorem eulerCarrierRadius_pos and the scalar gap definition eulerScalarGap, which packages the carrier log-derivative bound, the radius, and the carrier value into a single dimensionless quantity. This step supports the chain showing that realizable Euler ledgers cannot approach the T1 boundary x = 0, advancing the unified architecture toward a T1-bounded Riemann hypothesis statement inside Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.