def
definition
ga_capture_predicted
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Experimental.GalliumAnomaly on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
39
40/-- Standard Model prediction for Ga (SNU).
41 Value: ~74 SNU (BP04 solar model) -/
42noncomputable def ga_capture_predicted : ℝ := 74.0
43
44/-- The capture ratio: measured/predicted.
45 Value: ~0.78 (~22% deficit) -/
46noncomputable def ga_capture_ratio : ℝ := ga_capture_measured / ga_capture_predicted
47
48/-- **THEOREM EA-003.1**: The deficit is real (~20%). -/
49theorem deficit_real : ga_capture_ratio < 0.85 := by
50 unfold ga_capture_ratio ga_capture_measured ga_capture_predicted
51 norm_num
52
53/-- **THEOREM EA-003.2**: The deficit is bounded (not catastrophic).
54 Ratio > 0.70 means ~30% max deficit. -/
55theorem deficit_bounded : ga_capture_ratio > 0.70 := by
56 unfold ga_capture_ratio ga_capture_measured ga_capture_predicted
57 norm_num
58
59/-! ## II. The φ-Ladder Structure -/
60
61/-- Gallium rung on the φ-ladder (from mass ~70 u). -/
62noncomputable def gallium_rung : ℕ := 45
63
64/-- The φ-suppression factor for Ga. -/
65noncomputable def phi_suppression_ga : ℝ := phi ^ (-(gallium_rung : ℝ) / 10)
66
67/-- **THEOREM EA-003.3**: The φ-suppression is bounded.
68 φ^(-4.5) ∈ (0, 1) -/
69theorem phi_suppression_bounded : phi_suppression_ga > 0 ∧ phi_suppression_ga < 1 := by
70 have heq : phi_suppression_ga = phi ^ (-4.5 : ℝ) := by
71 unfold phi_suppression_ga gallium_rung
72 norm_num