shadow_fringe_observable_trivial
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not require res to be positive.
- Does not derive lambda_fringe from the eight-tick cycle or phi-ladder.
- Does not model the physical origin of the fringe frequency.
- Does not invoke the Recognition Composition Law.
formal statement (Lean)
111theorem shadow_fringe_observable_trivial (res : ℝ) :
112 ∃ lambda_fringe : ℝ, lambda_fringe > res := by
proof body
Term-mode proof.
113 use res + 1
114 linarith
115
116/-- **EXPERIMENTAL PREDICTION: Shadow Fringe Frequency**
117 The interference fringe at the event horizon has a fundamental
118 frequency determined by the 8-tick cycle. -/