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

Environment

show as:
view Lean formalization →

Environment packages a macroscopic bath as a record of degrees-of-freedom count, positive temperature, and coupling strength. Quantum decoherence calculations in Recognition Science cite this record when constructing pointer-state selection from J-cost minima. The declaration is a plain structure definition carrying one positivity constraint.

claimAn environment is a triple $(N, T, g)$ where $N$ is a natural number of degrees of freedom, $T > 0$ is temperature, and $g$ is interaction strength.

background

The module QF-003 derives pointer states as the stable configurations that minimize J-cost under environmental coupling. Pointer states correspond to neutral windows in the J-cost landscape; superpositions acquire high J-cost through entanglement and are suppressed. Upstream, the actualization operator A maps a configuration to the J-minimizing outcome, while temperature is recovered as the inverse Lagrange multiplier from the Boltzmann distribution.

proof idea

This is a structure definition that directly assembles the three parameters together with the temperature positivity field.

why it matters in Recognition Science

The record supplies the environment model required by einselection_from_jcost and decoherenceTime. It fills the QF-003 target of obtaining classical pointer states from neutral windows in the J-cost landscape. The same structure appears in the continuous quantum-to-classical crossover that depends on system size, temperature, and coupling.

scope and limits

formal statement (Lean)

  56structure Environment where
  57  degrees_of_freedom : ℕ
  58  temperature : ℝ
  59  interaction_strength : ℝ
  60  temp_pos : temperature > 0
  61
  62/-- A typical macroscopic environment (room temperature, many particles). -/

used by (9)

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

depends on (4)

Lean names referenced from this declaration's body.