theorem
proved
term proof
pbh_shadow_detectable
show as:
view Lean formalization →
formal statement (Lean)
69theorem pbh_shadow_detectable (Rs lambda_rec : ℝ) (h_Rs : Rs = 1e-6) (h_lambda : lambda_rec = 1e-35) :
70 ∃ (epsilon : ℝ), epsilon = lambda_rec / Rs ∧ epsilon = 1e-29 := by
proof body
Term-mode proof.
71 use lambda_rec / Rs
72 constructor
73 · rfl
74 · rw [h_Rs, h_lambda]
75 norm_num
76
77/-- **HYPOTHESIS**: Shadow Fringe Observability.
78
79 STATUS: EMPIRICAL_HYPOTHESIS — This is a testable prediction about
80 future EHT-class observations, not a mathematical theorem.
81
82 The prediction: For sufficiently small Rs/dist (primordial black holes),
83 the 8-tick phase fringe could produce detectable spatial modulation.
84
85 FALSIFIER: If high-precision shadow observations show NO fringe structure
86 at the predicted wavelength, this prediction is falsified.
87
88 TODO: The mapping from temporal frequency (1/8τ₀) to spatial wavelength
89 depends on the specific geodesic structure near the horizon. -/