structure
definition
def or abbrev
DefectSensor
show as:
view Lean formalization →
formal statement (Lean)
103structure DefectSensor where
104 /-- The multiplicity of the zero (= order of the pole of ζ⁻¹). -/
105 charge : ℤ
106 /-- The real part of the zero location. -/
107 realPart : ℝ
108 /-- The zero is in the right half of the critical strip. -/
109 in_strip : 1/2 < realPart ∧ realPart < 1
110
111/-! ### §3. The explicit cost-covering package -/
112
113/-- An explicit carrier package for the RS cost-covering bridge.
114
115This is the honest replacement for the former naked axiom. Any consumer of the
116bridge must now supply a concrete `BudgetedCarrier` witness for the realized
117carrier trace. -/
used by (40)
-
analytic_rh -
carrier_side_obstruction -
charge_zero_of_covered -
floorCovered_iff_charge_zero -
rh_chain_summary_legacy -
argument_principle_honest -
argument_principle_trivial -
honest_argument_principle_phase_family -
rh_from_single_axiom -
ArgumentPrincipleSensorCert -
zeta_zero_gives_charged_sensor -
boundaryTransportCert_iff_rh_core -
divergence_witnesses_boundary_of_cert -
no_cost_divergent_sensor_of_boundary_transport -
carrier_defect_budget_contradiction -
carrier_defect_comparison_rh -
defect_cost_exceeds_carrier_budget -
defect_floor_exceeds_any_bound -
mkSharedCirclePair -
mkSharedCirclePair_carrier_excess_bounded -
SharedCircleFamilyPair -
primeEulerEvent_mem_sensorEulerLedger -
reciprocal_primeEulerEvent_mem_sensorEulerLedger -
sensorEulerLedger -
sensorEulerLedger_balanced -
sensorEulerLedger_cost_formula -
sensorEulerLedger_identification -
sensorEulerLedger_net_flow_zero -
sensor_realPart_pos -
defectWindingData