No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
184def constructive_interference (path1 path2 : List Config) : Prop :=
proof body
Definition body.
185 ∃ n : ℤ, interference_amplitude path1 path2 (2 * Real.pi * n) > 0
186
187/-- **DESTRUCTIVE INTERFERENCE**: When paths cancel.
188
189 Occurs when phase_diff = π(2n+1) (paths out of phase). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (10)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
Config
in IndisputableMonolith.Gravity.ILG
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
interference_amplitude
in IndisputableMonolith.Modal.ModalGeometry
decl_use
-
Config
in IndisputableMonolith.Modal.Possibility
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use