theorem
proved
realizedDefectCollapseBoundaryApproaching_of_nonzero_charge
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Unification.UnifiedRH on GitHub at line 356.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
lt_trans -
one_mul -
of -
defect -
of -
of -
of -
annularCost -
DefectSensor -
canonicalDefectSampledFamily -
canonicalDefectSampledFamily_sensor -
defectSampledFamily_unbounded -
annularCost_nonneg -
RealizedCollapseBoundaryApproaching -
realizedDefectCollapseScalar
used by
formal source
353/-- The canonical realized-defect collapse scalar approaches the T1 boundary
354`0` for every nonzero-charge sensor. This is the concrete quantitative
355collapse mechanism replacing the old structural axiom. -/
356theorem realizedDefectCollapseBoundaryApproaching_of_nonzero_charge
357 (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
358 RealizedCollapseBoundaryApproaching sensor hm := by
359 intro ε hε
360 let fam := canonicalDefectSampledFamily sensor hm
361 have hfam : fam.sensor.charge ≠ 0 := by
362 simpa [fam, canonicalDefectSampledFamily_sensor] using hm
363 by_cases hεle : ε ≤ 1
364 · let B : ℝ := ε⁻¹ - 1
365 obtain ⟨N, hN⟩ := defectSampledFamily_unbounded fam hfam B
366 refine ⟨N, ?_⟩
367 unfold realizedDefectCollapseScalar
368 dsimp [fam, B] at hN ⊢
369 have hden_pos : 0 < 1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) := by
370 have hcost_nonneg :
371 0 ≤ annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) :=
372 annularCost_nonneg _
373 linarith
374 have hmul :
375 1 < ε * (1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N)) := by
376 have hgt : ε⁻¹ < 1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N) := by
377 linarith
378 have hεpos : 0 < ε := hε
379 have htmp := mul_lt_mul_of_pos_left hgt hεpos
380 have hleft : ε * ε⁻¹ = 1 := by
381 field_simp [hε.ne']
382 calc
383 1 = ε * ε⁻¹ := hleft.symm
384 _ < ε * (1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N)) := htmp
385 rw [div_lt_iff₀ hden_pos]
386 exact hmul