shadow_fringe_frequency_identity
plain-language theorem explainer
The identity shows that the frequency of the interference fringe around a black hole shadow equals the reciprocal of eight times the fundamental tick duration τ₀. Researchers modeling ILG-corrected lensing in Recognition Science would cite this when linking the eight-tick cycle to observable phase fringes. The proof is a one-line reflexivity step that matches the definition of the fringe frequency exactly.
Claim. For fundamental tick duration τ₀ > 0, the shadow fringe frequency satisfies f = 1/(8 τ₀).
background
The module develops black hole shadow predictions under the Recognition Science framework, where the eight-tick octave (period 2³) produces a detectable phase fringe at the event horizon. ShadowFringeFrequency is defined directly as 1/(8 τ₀), with τ₀ the basic time unit supplied by upstream constants modules (including derivations from ħ, G, and c). The local setting is the formalization of ILG-corrected lensing effects that follow from the forcing chain through T7.
proof idea
The proof is a one-line reflexivity tactic that matches the definition of ShadowFringeFrequency exactly.
why it matters
This identity anchors the experimental prediction that the eight-tick cycle produces a fringe frequency in black hole shadows. It supplies the direct link from T7 (eight-tick octave) to the lensing observables in the Relativity.Lensing module. No downstream uses are recorded yet, and the result remains definitional with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.