pith. sign in
module module moderate

IndisputableMonolith.Physics.CriticalPhenomenaFromJCost

show as:
view Lean formalization →

This module derives critical phenomena in physics from the J-cost function by instantiating the canonical six-clause J-band template. It introduces UniversalityClass and CriticalPhenomenaCert as the core objects. Condensed-matter physicists would cite it to link phase transitions to the Recognition Science forcing chain. The module applies the reusable J-cost template from CanonicalJBand as a definition layer with no internal proofs.

claimThe critical phenomena certificate asserts that the J-cost function on ratios satisfies $J(1)=0$ and $J(x)geq 0$ for $x>0$, yielding a universality class count for phase transitions.

background

The module sits inside the Recognition Science master cert chain and imports the Canonical J-Cost Band template. That template supplies the six-clause J-cost-on-ratio structure used for all domain certificates: matched-zero at J(1)=0 together with nonnegativity J(x)geq 0 for x>0. The local setting is therefore the application of this reusable band to critical phenomena, with sibling definitions UniversalityClass and CriticalPhenomenaCert serving as the concrete instantiations.

proof idea

This is a definition module, no proofs. It directly re-exports and specializes the six-clause template supplied by the upstream CanonicalJBand import.

why it matters in Recognition Science

The module supplies the physics-domain certificate that feeds the master cert chain for B-tier whole-science openings. It closes the critical-phenomena slot in the Plan v7 domain certs by instantiating the J-cost band, thereby connecting phase-transition universality to the J-uniqueness and phi fixed-point steps of the forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)