def
definition
def or abbrev
experiments
show as:
view Lean formalization →
formal statement (Lean)
232def experiments : List String := [
proof body
Definition body.
233 "Young's double-slit (1801)",
234 "Davisson-Germer electron diffraction (1927)",
235 "Fullerene interference (1999)",
236 "Delayed-choice quantum eraser (2000s)"
237]
238
239/-! ## Falsification Criteria -/
240
241/-- The double-slit derivation would be falsified by:
242 1. No interference for particles
243 2. Which-path info not affecting pattern
244 3. Quantum eraser not working
245 4. Phase not related to path length -/
used by (26)
-
curvature_defect_strength -
defect_site_prediction -
dama_not_dark_matter_in_rs -
substrate_model -
energy_conservation -
m_coh_positive -
equivalence_implies_ratio_one -
H_GravitationalRunning_certificate -
experimentalStatus -
quantum_requires_complex -
BellFalsifier -
loopholeFreeExperiment -
rsPredictions -
experimentalStatus -
experiments -
predictions -
experimentalTests -
possibleTests -
relativity_preserved -
experiments -
experimentalEvidence -
quadratic_from_symmetry -
shadow_diameter_correction -
deltaCP_pmns_range -
experiments -
experimentalStatus