fringe_frequency_grounded
plain-language theorem explainer
The theorem establishes that the shadow fringe frequency 1/(8 tau0) is strictly positive whenever the fundamental tick duration tau0 exceeds zero. Researchers modeling black hole shadows under the Recognition Science eight-tick cycle would cite this to confirm the predicted interference frequency is physically admissible. The proof reduces immediately to unfolding the frequency definition and invoking the positivity tactic on the resulting positive reciprocal.
Claim. Let $tau_0 > 0$ denote the fundamental tick duration. Then the shadow fringe frequency defined by $1/(8 tau_0)$ satisfies $1/(8 tau_0) > 0$.
background
The module formalizes ILG-corrected lensing predictions for black hole shadows, with the explicit objective of proving that the 8-tick cycle produces a detectable phase fringe at the event horizon. The constant tau0 is introduced in Constants as the duration of one fundamental tick in RS-native units, appearing in multiple derivations including the square-root expression involving hbar, G, and c. ShadowFringeFrequency is defined directly as the reciprocal 1/(8 * tau0), encoding the interference frequency forced by the eight-tick octave.
proof idea
The term-mode proof unfolds ShadowFringeFrequency to expose the explicit form 1/(8 * tau0), after which the positivity tactic is applied. This succeeds because the hypothesis tau0 > 0 makes the denominator positive, hence the entire expression positive.
why it matters
The declaration supplies the basic positivity guarantee required by the module's goal of establishing observable phase fringes from the 8-tick cycle. It directly instantiates the T7 eight-tick octave landmark of the Recognition Science forcing chain and serves as a prerequisite for any subsequent lensing corrections or observability statements in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.