experiments
plain-language theorem explainer
The experiments definition enumerates four laboratory signatures that test whether classical behavior emerges from many-body J-cost minimization. Optomechanics and quantum-foundations researchers would cite the list when benchmarking Recognition Science predictions against macroscopic coherence data. It is a direct list definition with no lemmas or reductions.
Claim. The list of experimental tests for classical emergence via J-cost minimization is: Fullerene interference (Zeilinger), LIGO mirrors (quantum noise limited), Optomechanical cooling, Quantum gases in traps.
background
Module QF-011 derives classical emergence from many-body J-cost minimization. Single-particle states allow superpositions at low cost; correlated many-body states incur J-cost scaling as N² while product states scale only as N. For large N the minimum is therefore classical. The upstream cost definitions supply the J-cost: one from MultiplicativeRecognizerL4 as derivedCost on positive ratios, another from ObserverForcing as Jcost of a RecognitionEvent. Sibling definitions in the same module (jcostProduct, jcostEntangled, einselection_from_jcost) formalize the quadratic penalty on entanglement.
proof idea
Direct definition of the List String; no lemmas applied and no tactics used.
why it matters
The list supplies the concrete experimental anchors for QF-011 and is referenced by twenty-six downstream declarations, including curvature_defect_strength and defect_site_prediction in ANITAUpgoing, dama_not_dark_matter_in_rs and substrate_model in DAMAModulation, energy_conservation in Hamiltonian, and m_coh_positive in CoherenceCollapse. It therefore closes the experimental interface for the many-body J-cost mechanism that selects pointer states and enforces the classical limit at large N.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.