IndisputableMonolith.NumberTheory.DefectSampledTrace

declarations in this module (25)

• def defectAnnularMesh L40
• theorem defectAnnularMesh_charge L49
• structure DefectSampledFamily L60
• def chosenDefectPhaseFamily L77
• theorem chosenDefectPhaseFamily_sensor L82
• def chosenDefectPhasePerturbationWitness L89
• def canonicalDefectSampledFamily L96
• theorem canonicalDefectSampledFamily_sensor L101
• theorem canonicalDefectSampledFamily_charge L107
• def RealizedDefectAnnularCostBounded L118
• def RealizedDefectAnnularExcessBounded L125
• structure RingRegularErrorBound L138
• def realizedRingPerturbationError L151
• structure RingPerturbationControl L171
• def ringRegularErrorBound_of_ringPerturbationControl L181
• theorem annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError L217
• theorem realizedDefectAnnularExcessBounded_of_ringRegularErrorBound L242
• theorem realizedDefectAnnularExcessBounded_of_costBounded L254
• theorem realizedDefectCostBounded_of_charge_zero_and_excessBounded L270
• theorem realizedDefectCostBounded_iff_charge_zero_and_excessBounded L294
• def canonicalDefectSampledFamily_ringPerturbationControl L322
• def canonicalDefectSampledFamily_ringRegularErrorBound L432
• theorem canonicalDefectSampledFamily_excess_bounded L438
• theorem defectSampledFamily_unbounded L449
• theorem not_realizedDefectAnnularCostBounded L462