shadow_fringe_observable_trivial
plain-language theorem explainer
For any real resolution threshold res there exists a fringe wavelength exceeding it. Researchers modeling black hole shadows under the Recognition Science eight-tick cycle cite this to guarantee that phase fringes remain detectable above any given resolution. The proof is a one-line term-mode construction that instantiates the witness as res plus one and discharges the inequality via linear arithmetic.
Claim. For any real number $res$, there exists a real number $lambda_{fringe}$ such that $lambda_{fringe} > res$.
background
The module formalizes ILG-corrected lensing predictions for black hole shadows, with the objective of showing that the eight-tick cycle produces a detectable phase fringe at the event horizon. The fundamental RS time quantum is the tick, defined as the constant 1 with notation tau_0, while Frequency is an abbreviation for the reals. Upstream results supply the tick definition as the RS-native time quantum and the has class for spectral peaks ranked by phi-rung, though the latter is unused in this declaration.
proof idea
Term-mode proof that applies the existential introduction tactic with the concrete witness res + 1, then invokes linarith to verify the strict inequality.
why it matters
The result supplies a pure existence guarantee inside the shadow predictions module, supporting the claim that the eight-tick cycle (T7) yields observable fringes. No parent theorems or downstream uses are recorded, leaving open its integration with frequency identities or lensing corrections elsewhere in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.