pith. machine review for the scientific record. sign in
def definition def or abbrev high

experiments

show as:
view Lean formalization →

The declaration enumerates four experimental tests validating classical emergence from many-body J-cost minimization in Recognition Science. Quantum foundations researchers and optomechanics experimentalists would cite it when assessing macroscopic decoherence predictions. It is assembled as a direct list definition that cross-references experiment catalogs from DoubleSlit and PlanckScale modules.

claimThe experiments supporting classical emergence via J-cost minimization are the list consisting of fullerene interference (C₆₀), LIGO mirrors at quantum noise limit, optomechanical cooling of macroscopic objects, and quantum gases in traps.

background

Recognition Science derives classical behavior from many-body J-cost minimization: single-particle superpositions carry low cost while correlated many-body states scale quadratically or worse, so product states minimize total cost at large N. The J-cost function is the derived cost of a multiplicative recognizer's comparator on positive ratios, as defined in MultiplicativeRecognizerL4.cost and ObserverForcing.cost. This module (QF-011) supplies the empirical anchor list for that mechanism, drawing on upstream experiment enumerations from DoubleSlit and PlanckScale.

proof idea

The definition is a direct enumeration of four strings. It assembles the list by referencing the experiment definitions in DoubleSlit.experiments and PlanckScale.experiments, then adds the two additional macroscopic tests required for the classical-emergence claim.

why it matters in Recognition Science

This definition supplies the experimental grounding for the QF-011 derivation of classical emergence and is referenced by downstream results including ANITAUpgoing.curvature_defect_strength, DAMAModulation.dama_not_dark_matter_in_rs, and Gravity.CoherenceCollapse.m_coh_positive. It anchors the J-cost scaling argument to concrete observations and connects to the Recognition forcing chain through the cost functions that appear in the T5 J-uniqueness and T6 phi fixed-point steps.

scope and limits

formal statement (Lean)

 211def experiments : List String := [

proof body

Definition body.

 212  "Fullerene interference (Zeilinger)",
 213  "LIGO mirrors (quantum noise limited)",
 214  "Optomechanical cooling",
 215  "Quantum gases in traps"
 216]
 217
 218/-! ## Falsification Criteria -/
 219
 220/-- The classical emergence derivation would be falsified by:
 221    1. Macroscopic quantum superpositions persisting
 222    2. Decoherence not depending on system size
 223    3. Pointer states not being J-cost minima
 224    4. Classical physics failing at large N -/

used by (26)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.