pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.CondensedMatter.JCostPhaseTransition

show as:
view Lean formalization →

This module defines the canonical J-cost function J(x) = (x + x^{-1})/2 - 1 together with derived scales for phase transitions in condensed matter. Researchers working on superconducting gaps or critical temperatures in RS-native units would cite these objects. The module consists entirely of definitions and supporting properties for symmetry and positivity, with no theorems proved.

claimThe J-cost function is defined by $J(x) = (x + x^{-1})/2 - 1$. Derived objects include the critical energy scale, superconducting gap scale, and critical temperature $T_c$ expressed on the phi-ladder.

background

Recognition Science fixes the J-cost via T5 uniqueness as J(x) = (x + x^{-1})/2 - 1, equivalently cosh(log x) - 1. This module sits in the CondensedMatter domain and imports the base time quantum τ₀ = 1 tick from Constants. It introduces J_cost along with phi_critical_energy, sc_gap_scale, and T_critical to quantify phase transitions using the phi self-similar fixed point and eight-tick octave.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the J-cost and critical energy definitions that support condensed matter applications of the Recognition framework, including gap and temperature predictions. It rests on the forcing chain T5-T8 and the Recognition Composition Law. No downstream declarations are listed.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)