`phi_pow_residue_mu_upper`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.LeptonGenerations.Necessity
domain: Physics
line: 570 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.LeptonGenerations.Necessity on GitHub at line 570.

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

 567        simpa [phi_pow_neg963_lower_hypothesis] using phi_pow_neg963_lower_proved
 568    _ < Real.goldenRatio ^ predicted_residue_mu := h_lt
 569
 570theorem phi_pow_residue_mu_upper :
 571    phi ^ predicted_residue_mu < (0.0098 : ℝ) := by
 572  have h_mu := predicted_residue_mu_bounds
 573  have h_phi_gt : phi = Real.goldenRatio := rfl
 574  rw [h_phi_gt]
 575  have h_mono := Numerics.phi_rpow_strictMono
 576  have h_lt : Real.goldenRatio ^ predicted_residue_mu < Real.goldenRatio ^ (-9.62 : ℝ) :=
 577    h_mono h_mu.2
 578  calc Real.goldenRatio ^ predicted_residue_mu < Real.goldenRatio ^ (-9.62 : ℝ) := h_lt
 579    _ < (0.0098 : ℝ) := by
 580        simpa [phi_pow_neg962_upper_hypothesis] using phi_pow_neg962_upper_proved
 581
 582/-- Bounds on φ^(predicted_residue_mu). -/
 583lemma phi_pow_residue_mu_bounds :
 584    (0.0097 : ℝ) < phi ^ predicted_residue_mu ∧ phi ^ predicted_residue_mu < (0.0098 : ℝ) :=
 585  ⟨phi_pow_residue_mu_lower,
 586   phi_pow_residue_mu_upper⟩
 587
 588/-! CORRECTED: φ^(predicted_residue_tau) where residue_tau ∈ (-3.77, -3.75)
 589Previous claim of 0.346 < φ^residue < 0.348 was FALSE!
 590Actual: φ^(-3.76) ≈ 0.164
 591Conservative seam bounds: φ^(-3.77) > 0.1629 and φ^(-3.75) < 0.165. -/
 592
 593/-- External numeric hypothesis: φ^(-3.77) > 0.1629. -/
 594def phi_pow_neg377_lower_hypothesis : Prop :=
 595  (0.1629 : ℝ) < Real.goldenRatio ^ (-3.77 : ℝ)
 596
 597/-- External numeric hypothesis: φ^(-3.75) < 0.165. -/
 598def phi_pow_neg375_upper_hypothesis : Prop :=
 599  Real.goldenRatio ^ (-3.75 : ℝ) < (0.165 : ℝ)
 600

papers checked against this theorem

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