theorem proved tactic proof

`shadow_fringe_wavelength_exists`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 102theorem shadow_fringe_wavelength_exists (Rs dist : ℝ) (h_Rs : Rs > 0) (h_dist : dist > 0) :
 103    let theta_Rs := Rs / dist

proof body

Tactic-mode proof.

 104    ∃ lambda_fringe : ℝ, lambda_fringe = c_SI * 8 * tau0 * theta_Rs := by
 105  use c_SI * 8 * tau0 * (Rs / dist)
 106
 107/-- **THEOREM (RIGOROUS)**: Observable fringe exists for any positive resolution threshold.
 108
 109    This is a pure existence result - given any resolution res > 0,
 110    we can find a wavelength that exceeds it. -/

depends on (16)

Lean names referenced from this declaration's body.

tau0 in IndisputableMonolith.Compat.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
c_SI in IndisputableMonolith.Constants.ExternalAnchors decl_use
c_SI in IndisputableMonolith.Cosmology.SIConversion decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
Observable in IndisputableMonolith.Foundation.RecognitionForcing decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
c_SI in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
Observable in IndisputableMonolith.Measurement.RSNative.Core decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
Observable in IndisputableMonolith.Quantum.Observables decl_use
c_SI in IndisputableMonolith.RRF.Foundation.Constants decl_use