CoherenceThreshold
plain-language theorem explainer
The CoherenceThreshold structure packages a positive critical temperature together with a coherence map normalized to one at that temperature. Workers on finite-temperature recognition dynamics cite it to separate the frozen coherent regime from the disordered classical regime. The definition is a direct bundling of the positivity axiom and the normalization condition with no lemmas or reductions required.
Claim. A coherence threshold consists of a positive real number $T_c > 0$ and a function $c : ℝ → ℝ$ such that $c(T_c) = 1$.
background
Recognition Thermodynamics extends the zero-temperature J-cost minimization to finite Recognition Temperature TR. The module introduces TR as the parameter controlling the strictness of J-minimization, the inverse beta, the Gibbs measure proportional to exp(-J(x)/TR), and the associated recognition entropy and free energy. The local setting ties these objects to the J-cost function J(x) = ½(x + 1/x) - 1 and the eight-tick cycle as the fundamental time unit.
proof idea
This is a structure definition that directly introduces the four fields: the critical temperature, its positivity, the coherence function, and the normalization condition at criticality. No tactics, lemmas, or reductions are applied; the fields stand as the interface to be instantiated by downstream constructions.
why it matters
The definition supplies the phase-transition interface for the thermodynamics module. It connects the J-cost phase transition scale (T_critical from CondensedMatter.JCostPhaseTransition) to the coherence parameter that marks the boundary between coherent and decoherent regimes. It prepares the ground for the Gibbs weights and entropy calculations appearing as sibling declarations in the same file, while leaving open its explicit linkage to the phi-ladder and eight-tick forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.