pith. sign in
module module high

IndisputableMonolith.CondensedMatter.JCostPhaseTransition

show as:
view Lean formalization →

This module defines the J-cost function J(x) = (x + x^{-1})/2 - 1 together with critical energy, gap scale, and temperature quantities for phase transitions. Condensed matter theorists applying Recognition Science to superconductivity or critical phenomena would cite these definitions. The module consists entirely of definitions with no theorems or proofs.

claim$J(x) = (x + x^{-1})/2 - 1$

background

Recognition Science starts from the forcing chain in IndisputableMonolith.Foundation.UnifiedForcingChain, where T5 fixes the J-uniqueness property J(x) = (x + x^{-1})/2 - 1. The module imports the RS time quantum τ₀ = 1 tick from Constants and Mathlib real-analysis primitives. It introduces J_cost as the canonical cost function, then defines phi_critical_energy, sc_gap_scale, T_critical, and predicates J_cost_minimum_at_one, J_cost_positive_away_from_one, J_cost_symmetric that locate the minimum at x = 1.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the J-cost and phase-transition primitives that later feed into condensed-matter predictions such as the superconducting gap and critical temperature. It directly instantiates the J-uniqueness step (T5) of the forcing chain for use in the phi-ladder and eight-tick octave structure.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)