EntropicCooling
plain-language theorem explainer
The declaration defines the entropic cooling condition as the implication that negative vacuum entropy change forces negative environmental heat change. Researchers modeling metric engines or RS thermodynamics would cite it as the core pump relation. The definition is a direct one-line implication on real numbers with no lemmas applied.
Claim. The entropic cooling condition asserts that if the vacuum entropy change satisfies $ΔS_ {vacuum} < 0$, then the environmental heat change satisfies $ΔQ_{env} < 0$.
background
In the Vacuum Pump module, Recognition Science models a metric engine that orders vacuum fluctuations, lowering the J-cost and absorbing heat from the environment. This reverses the usual thermodynamic arrow: vacuum ordering produces cooling rather than heat. The definition relies on the power spectrum from PrimordialSpectrum, which gives amplitude at wavenumber k as a power-law factor, and on the DomainBootstrap.required structure needed to state metric-engine conditions.
proof idea
The definition directly encodes the implication delta_S_vacuum < 0 → delta_Q_env < 0 as a primitive Prop on the reals; no lemmas or tactics are invoked.
why it matters
This supplies the thermodynamic relation for the entropic pump hypothesis in the Energy domain and underpins sibling declarations such as SelfSustaining and VacuumPower. It realizes the ordering-vacuum mechanism that absorbs environmental entropy, consistent with RS-native energy scaling on the phi-ladder. It remains a hypothesis interface; no downstream theorem yet discharges it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.