pith. sign in
module module low

IndisputableMonolith.Chemistry.EnvPressure

show as:
view Lean formalization →

The environmental pressure module in the Chemistry domain supplies definitions for scaling quantities used in Recognition Science models of chemical environments. It depends solely on the Constants module to access the fundamental time quantum. The module consists of three definitions and contains no theorems or proofs.

claimDefinitions of a scale factor, an energy rescaling operation, and a neutral-8 quantity for environmental pressure calculations, all expressed in RS-native units with $\tau_0 = 1$ tick.

background

Recognition Science derives all physics from one functional equation. The Constants module supplies the fundamental RS time quantum $\tau_0 = 1$ tick. This module operates in the chemistry domain, imports Mathlib for supporting structures, and introduces auxiliary definitions for scaling energies and pressures that build on the imported time quantum.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supply building blocks for chemical environment modeling that would feed into parent theorems on molecular interactions or phase behavior in the Recognition Science framework. No specific downstream theorems are recorded in the current dependency graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)