`modally_equivalent_symm`

proved

show as: view math explainer →

module: IndisputableMonolith.Modal.ModalGeometry
domain: Modal
line: 150 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Modal.ModalGeometry on GitHub at line 150.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 147  simp [modally_equivalent]
 148
 149/-- Modal equivalence is symmetric. -/
 150lemma modally_equivalent_symm (c1 c2 : Config) :
 151    modally_equivalent c1 c2 ↔ modally_equivalent c2 c1 := by
 152  simp [modally_equivalent]
 153  constructor <;> (intro ⟨h1, h2, h3⟩; exact ⟨h1.symm, h3, h2⟩)
 154
 155/-- **MODAL NYQUIST THEOREM**: The universe cannot distinguish possibilities
 156    finer than one tick.
 157
 158    This is the modal analog of:
 159    - Nyquist sampling (time)
 160    - Heisenberg uncertainty (phase space)
 161    - Gap-45 consciousness threshold (qualia)
 162
 163    The 8-tick structure forces this limit. -/
 164theorem modal_nyquist (c1 c2 : Config)
 165    (h_val : c1.value = c2.value)
 166    (h_time : c1.time = c2.time) :
 167    modally_equivalent c1 c2 := by
 168  simp [modally_equivalent, h_val, h_time]
 169
 170/-! ## Possibility Interference -/
 171
 172/-- **INTERFERENCE AMPLITUDE**: The overlap between two possibility paths.
 173
 174    When two paths have similar cost, they can "interfere."
 175    I(γ₁, γ₂) = √(W[γ₁] · W[γ₂]) · cos(Δφ)
 176
 177    where Δφ is the phase difference. -/
 178noncomputable def interference_amplitude (path1 path2 : List Config) (phase_diff : ℝ) : ℝ :=
 179  Real.sqrt (PathWeight path1 * PathWeight path2) * Real.cos phase_diff
 180

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.