defect_bounded_impossible

formal source

 859/-- The conditional floor-covering theorem is also derivable: if the defect cost
 860is bounded along the canonical realized trace, then nonzero charge is
 861impossible. -/
 862theorem defect_bounded_impossible (sensor : DefectSensor)
 863    (hm : sensor.charge ≠ 0)
 864    (hbound : RealizedDefectAnnularCostBounded
 865      (canonicalDefectSampledFamily sensor hm)) :
 866    False := by
 867  let fam := canonicalDefectSampledFamily sensor hm
 868  have hfam : fam.sensor.charge ≠ 0 := by
 869    simpa [fam, canonicalDefectSampledFamily_sensor] using hm
 870  exact not_realizedDefectAnnularCostBounded fam hfam hbound
 871
 872/-! ### §8. The defect sensor for ζ -/
 873
 874/-- Given a hypothetical zero of ζ at s = ρ with Re(ρ) > 1/2
 875    and multiplicity m ≥ 1, construct the DefectSensor. -/
 876def zetaDefectSensor (realPart : ℝ) (h_strip : 1/2 < realPart ∧ realPart < 1)
 877    (multiplicity : ℤ) : DefectSensor where
 878  charge := multiplicity
 879  realPart := realPart
 880  in_strip := h_strip
 881
 882/-- The sensor/carrier compatibility: the carrier is regular in
 883    a neighborhood of any hypothetical zero.
 884    Specifically: if Re(ρ) = σ₀ > 1/2, then D(ρ, σ₀ − 1/2) ⊂ {Re(s) > 1/2}
 885    and the carrier is holomorphic nonvanishing on this disk. -/
 886theorem sensor_carrier_compatible (sensor : DefectSensor) :
 887    ∃ (carrier : RegularCarrier),
 888      carrier.radius = sensor.realPart - 1/2 ∧
 889      0 < carrier.radius := by
 890  exact ⟨eulerRegularCarrier sensor.realPart sensor.in_strip.1,
 891         euler_regular_carrier_covers_strip sensor.realPart sensor.in_strip.1,
 892         by