def
definition
qlf_regularFactorPhase
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 457.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
454/-- Build a `RegularFactorPhase` from a `QuantitativeLocalFactorization`
455at a given level. This is the genuine Lipschitz-controlled phase of the
456regular factor on the `n`th circle. -/
457noncomputable def qlf_regularFactorPhase
458 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
459 RegularFactorPhase := by
460 have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
461 have hd : (0 : ℝ) < ↑n + 1 := by linarith
462 have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
463 exact regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
464 (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
465 qlf.logDerivBound qlf.logDerivBound_pos
466
467/-- A defect phase family using genuine regular-factor phase data.
468Each level carries non-trivial perturbation from the regular factor's
469Lipschitz-controlled phase, unlike the synthetic `zetaDerivedPhaseFamily`
470which has identically zero perturbation. -/
471noncomputable def genuineZetaDerivedPhaseFamily
472 (sensor : DefectSensor)
473 (qlf : QuantitativeLocalFactorization)
474 (horder : qlf.order = -sensor.charge) : DefectPhaseFamily where
475 sensor := sensor
476 witnessRadius := qlf.radius
477 witnessRadius_pos := qlf.radius_pos
478 phaseAtLevel n hn := genuineZetaDerivedPhaseData qlf n hn
479 charge_uniform n hn := by
480 have := genuineZetaDerivedPhaseData_charge qlf n hn
481 rw [this, horder, neg_neg]
482
483/-! ### §5b. Perturbation witness for genuine phase family -/
484
485/-- Extract the regular factor phase at level `n` from the genuine family. -/
486noncomputable def genuineRegularFactorPhaseAt
487 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :