pbh_shadow_detectable
plain-language theorem explainer
The declaration establishes that for a primordial black hole with Schwarzschild radius Rs equal to 10^{-6} and recognition wavelength lambda_rec equal to 10^{-35}, the relative correction epsilon equals 10^{-29}. Researchers modeling black hole shadows under Recognition Science corrections would cite this when setting detectability thresholds for future EHT-class instruments. The proof is a direct term construction that substitutes the ratio and evaluates it numerically under the supplied equalities.
Claim. For Schwarzschild radius $R_s = 10^{-6}$ and recognition wavelength $lambda_{rec} = 10^{-35}$, there exists $epsilon in mathbb{R}$ such that $epsilon = lambda_{rec}/R_s$ and $epsilon = 10^{-29}$.
background
The module formalizes ILG-corrected lensing predictions for black hole shadows, with the objective of showing that the 8-tick cycle produces a detectable phase fringe at the event horizon. Upstream definitions supply lambda_rec as the recognition length sqrt(hbar G / c^3) (equivalently ell_0 in RS-native units) and tick as the fundamental time quantum tau_0 = 1. The EightTick.phase definition supplies the periodic structure k pi / 4 for k = 0 to 7 that underlies fringe formation.
proof idea
The term proof introduces epsilon as the ratio lambda_rec / Rs, applies constructor to split the conjunction, uses rfl for the first equality, then rewrites the two hypotheses and invokes norm_num to confirm the numerical value of the division.
why it matters
This concrete instance supports the module's claim that the 8-tick octave (T7) yields an observable spatial modulation for sufficiently small Rs. It feeds the hypothesis interface for shadow fringe observability and supplies a numerical anchor for the alpha band and phi-ladder mass formula. The result leaves open the precise mapping from temporal frequency 1/8 tau_0 to spatial wavelength via geodesic structure near the horizon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.