DefectSampledFamily

formal source

  57Unlike a bare `AnnularTrace`, this object is intended to arise from the actual
  58phase-sampling construction for `ζ⁻¹`, not from an arbitrary synthetic mesh
  59family. -/
  60structure DefectSampledFamily where
  61  sensor : DefectSensor
  62  mesh : ∀ N : ℕ, AnnularMesh N
  63  charge_spec : ∀ N : ℕ, (mesh N).charge = sensor.charge
  64
  65/-- Convert a `DefectPhaseFamily` to its realized sampled annular family. -/
  66def DefectPhaseFamily.toSampledFamily (dpf : DefectPhaseFamily) :
  67    DefectSampledFamily where
  68  sensor := dpf.sensor
  69  mesh := defectAnnularMesh dpf
  70  charge_spec := defectAnnularMesh_charge dpf
  71
  72/-- Choose one phase family attached to a hypothetical defect sensor.
  73
  74This uses the strengthened existential package
  75`defect_phase_family_with_perturbation_exists`, so the chosen family comes with
  76the perturbation witness needed downstream for the annular excess argument. -/
  77noncomputable def chosenDefectPhaseFamily (sensor : DefectSensor)
  78    (hm : sensor.charge ≠ 0) : DefectPhaseFamily :=
  79  Classical.choose (defect_phase_family_with_perturbation_exists sensor hm)
  80
  81/-- The chosen phase family is attached to the requested sensor. -/
  82theorem chosenDefectPhaseFamily_sensor (sensor : DefectSensor)
  83    (hm : sensor.charge ≠ 0) :
  84    (chosenDefectPhaseFamily sensor hm).sensor = sensor :=
  85  (Classical.choose_spec (defect_phase_family_with_perturbation_exists sensor hm)).1
  86
  87/-- The chosen phase family also carries the regular-factor perturbation witness
  88needed to build the ring perturbation control package. -/
  89noncomputable def chosenDefectPhasePerturbationWitness (sensor : DefectSensor)
  90    (hm : sensor.charge ≠ 0) :