roomEnvironment
plain-language theorem explainer
A concrete instance of the Environment structure with 10^23 degrees of freedom, temperature 300, and interaction strength 0.1. Researchers modeling decoherence via J-cost minimization in Recognition Science cite this example to illustrate a typical macroscopic setting. The definition is a direct structure literal whose sole proof obligation is discharged by norm_num.
Claim. Let $E$ be the environment with $10^{23}$ degrees of freedom, temperature $300$, interaction strength $0.1$, and temperature strictly positive.
background
The Environment structure in this module consists of a natural number of degrees of freedom, a positive real temperature, a real interaction strength, and a positivity witness. This models a macroscopic bath that interacts with a quantum system and drives it toward configurations of locally minimal J-cost. The module setting QF-003 frames pointer states as the stable outcomes of such interactions, where superpositions incur higher J-cost through entanglement with the environment.
proof idea
The definition directly constructs the Environment record with the supplied numerical fields. The temperature positivity field is discharged by the norm_num tactic.
why it matters
This supplies a standard macroscopic example for the neutral-window mechanism in pointer-state emergence. It supports sibling results on predictability sieves and Lindblad eigenstates by providing concrete parameters for J-cost calculations. In the broader framework it instantiates the environment-interaction step that selects minimal-J-cost states, consistent with the cost definitions from ObserverForcing and MultiplicativeRecognizerL4, while leaving open how the specific numerical values arise from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.