MetastableState
plain-language theorem explainer
MetastableState packages a local J-cost minimum, global J-cost minimum, barrier height, and nucleation lifetime into a single structure. Researchers working on first-order phase transitions in Recognition Science cite it to represent supercooled liquids or supersaturated vapors trapped away from the global minimum. The definition simply assembles four real-valued fields drawn from the cost functions and phi-ladder lifetime.
Claim. A metastable state is a quadruple $(J_0, J_g, B, T)$ of real numbers where $J_0$ is the J-cost at a local minimum, $J_g$ is the J-cost at the global minimum, $B$ is the barrier height separating them, and $T$ is the lifetime until nucleation.
background
J-cost is the cost of a recognition event, defined as the derived cost of a multiplicative recognizer comparator or directly as Cost.Jcost on a state. Time is the native unit abbrev for real numbers. Lifetime is taken from the phi-ladder as phi raised to a rung index. The module derives phase transitions from bifurcations in the J-cost landscape, where multiple local minima appear and the system can remain trapped in a non-global minimum.
proof idea
The declaration is a structure definition that directly assembles the four real fields with no lemmas or tactics applied.
why it matters
It supplies the data type needed to encode metastable states for the first-order transition mechanism in the J-cost bifurcation framework. The module targets derivation of discontinuous changes such as melting from local minima separated by barriers, consistent with the Recognition Science program of obtaining thermodynamics from the forcing chain and cost functions. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.