`chosenDefectPhaseFamily`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.DefectSampledTrace
domain: NumberTheory
line: 77 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.DefectSampledTrace on GitHub at line 77.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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) :
  91    DefectPhasePerturbationWitness (chosenDefectPhaseFamily sensor hm) :=
  92  Classical.choice ((Classical.choose_spec
  93    (defect_phase_family_with_perturbation_exists sensor hm)).2)
  94
  95/-- The canonical realized sampled family attached to a hypothetical defect. -/
  96noncomputable def canonicalDefectSampledFamily (sensor : DefectSensor)
  97    (hm : sensor.charge ≠ 0) : DefectSampledFamily :=
  98  (chosenDefectPhaseFamily sensor hm).toSampledFamily
  99
 100/-- The canonical sampled family remembers the requested sensor. -/
 101theorem canonicalDefectSampledFamily_sensor (sensor : DefectSensor)
 102    (hm : sensor.charge ≠ 0) :
 103    (canonicalDefectSampledFamily sensor hm).sensor = sensor :=
 104  chosenDefectPhaseFamily_sensor sensor hm
 105
 106/-- Every mesh in the canonical sampled family has the requested sensor charge. -/
 107theorem canonicalDefectSampledFamily_charge (sensor : DefectSensor)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.