def definition def or abbrev

`H_ShadowFringeObservable`

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

formal statement (Lean)

  90def H_ShadowFringeObservable (Rs dist res : ℝ) : Prop :=

proof body

Definition body.

  91  let theta_Rs := Rs / dist
  92  let f_fringe := 1 / (8 * tau0)
  93  -- The fringe is observable if the spatial wavelength exceeds resolution
  94  ∃ lambda_fringe : ℝ, lambda_fringe > 0 ∧
  95    -- Physical constraint: wavelength is related to fringe frequency and light travel time
  96    lambda_fringe = c_SI / f_fringe * theta_Rs
  97
  98/-- **THEOREM (RIGOROUS)**: Existence of a spatial wavelength.
  99
 100    This proves that a spatial wavelength CAN be defined for any finite tau0.
 101    Whether it exceeds the resolution is an empirical question. -/

depends on (20)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Physical in IndisputableMonolith.Bridge.DataCore decl_use
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
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
c_SI in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
that in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
c_SI in IndisputableMonolith.RRF.Foundation.Constants decl_use