Pith. sign in
module module moderate

IndisputableMonolith.Physics.CriticalPhenomenaFromJCost

show as:
view Lean formalization →

The module applies the J-cost band template to derive critical phenomena in physics. It introduces universality classes and a certification structure based on the six-clause template. Researchers in statistical mechanics or recognition science would cite it when linking J-cost properties to phase transitions. The module organizes these as definitions and certificates without internal proofs.

claimThe module defines $\text{UniversalityClass}$ and $\text{CriticalPhenomenaCert}$ as instances of the J-cost band satisfying $J(1)=0$ and $J(x)\geq 0$ for $x>0$.

background

The upstream CanonicalJBand module supplies the reusable six-clause J-cost-on-ratio template for domain certificates across the master cert chain. Its clauses include matched-zero: $J(1)=0$ and nonneg: $J(x)\geq 0$ for $x>0$. This module applies that template within the physics domain to critical phenomena.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It contributes to the B-tier whole-science openings in the Plan v7 domain certificates by instantiating the J-cost template for critical phenomena. The module supports the overall recognition science framework for physics applications.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)