ShadowFringeFrequency
plain-language theorem explainer
ShadowFringeFrequency supplies the frequency of the interference fringe at a black hole event horizon as the reciprocal of eight times the fundamental tick duration tau0. Researchers modeling black hole shadows within Recognition Science would cite this when linking lensing predictions to the eight-tick octave. The definition is a direct algebraic encoding of the T7 forcing step with no further reduction required.
Claim. The shadow fringe frequency equals $1/(8 tau_0)$, where $tau_0$ is the fundamental tick duration in RS-native units.
background
The module formalizes ILG-corrected lensing predictions for black hole shadows, with the explicit objective of showing that the eight-tick cycle produces a detectable phase fringe at the event horizon. tau0 is the fundamental time quantum, defined as the duration of one tick in RS-native units and carried forward from the Constants module. The eight-tick period originates in the forcing chain as the octave of period 2^3 that sets the fundamental evolution scale.
proof idea
The definition is a direct algebraic expression that divides the reciprocal of tau0 by eight, implementing the eight-tick cycle without invoking any lemmas or tactics beyond the constant definitions of tick and tau0.
why it matters
This definition anchors the experimental predictions for black hole shadows. It is used directly by the theorems fringe_frequency_grounded and shadow_fringe_frequency_identity that establish positivity and the identity relation. It realizes the T7 eight-tick octave landmark inside the lensing context, supplying the concrete frequency scale for the phase fringe at the horizon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.