CriticalPoint
plain-language theorem explainer
The CriticalPoint structure records the temperature and pressure at which a first-order phase transition terminates, together with a Boolean flag marking the singularity. Researchers modeling J-cost bifurcations in Recognition Science thermodynamics would reference it to locate the endpoint of coexistence curves. The declaration is a plain record definition introducing three fields with no further axioms or computations.
Claim. A critical point is a triple $(T, P, s)$ with $T, P$ real numbers and $s$ a Boolean, marking the termination of a first-order transition line where the J-cost landscape changes topology.
background
The module derives phase transitions from bifurcations in the J-cost landscape, where multiple local minima merge or split as parameters vary and the system jumps between them. Temperature is defined as the inverse of the Lagrange multiplier beta. Pressure is given by the product of density, the kernel evaluation, and a scaling factor delta. The constant K is defined as the square root of phi, serving as a dimensionless bridge ratio.
proof idea
This is a structure definition that introduces the three fields temperature, pressure, and is_singular without any proof obligations or computational content.
why it matters
It supplies the data structure for the endpoint of first-order lines within the phase-transition theory built from J-cost bifurcations. The module targets derivation of such transitions as information-theoretic bifurcations, with the attached comment noting possible numerical links such as Tc/Tb ratios near sqrt(3) for water or phi/1.3 for helium. No downstream uses are recorded, leaving the precise embedding into the phi-ladder open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.