TopologicalTransition
TopologicalTransition packages a structure for phase transitions that alter the topology of the J-cost landscape rather than its symmetry. It records integer winding numbers before and after the change together with a continuity flag. Researchers modeling Kosterlitz-Thouless or topological insulator transitions in an information-theoretic setting would cite it when classifying critical points in the Recognition Science framework. The declaration is a plain structure definition with no computation or lemmas.
claimA topological transition is given by integers $n_b$ and $n_a$ for the winding numbers of the J-cost landscape before and after the transition, together with a boolean flag $c$ that is true precisely when the transition is continuous.
background
The module THERMO-006 treats phase transitions as bifurcations in the J-cost landscape whose local minima correspond to distinct phases. J-cost itself is the non-negative function Cost.Jcost applied to recognition events, as defined in ObserverForcing.cost, and is induced by multiplicative recognizers via MultiplicativeRecognizerL4.cost. The eight-tick phases from EightTick.phase supply the periodic calibration $kπ/4$ that underlies the landscape periodicity.
proof idea
This is a structure definition that directly assembles the three fields winding_number_before, winding_number_after, and is_continuous. No lemmas or tactics are invoked; the declaration simply declares the data type for later use in the phase-transition constructions of the module.
why it matters in Recognition Science
The structure supplies the classification of topological changes required by the module's target to derive phase transitions from J-cost bifurcations. It distinguishes cases such as Kosterlitz-Thouless transitions where the topology of the landscape changes, complementing the first-order and second-order mechanisms defined in sibling declarations. It thereby supports the broader Recognition Science program of obtaining all thermodynamics from the J-cost functional equation and the eight-tick octave.
scope and limits
- Does not compute winding numbers from an explicit J-cost function.
- Does not specify the spatial dimension or manifold on which the landscape is defined.
- Does not encode temperature dependence or nucleation rates.
- Does not distinguish first-order from second-order transitions.
formal statement (Lean)
226structure TopologicalTransition where
227 winding_number_before : ℤ
228 winding_number_after : ℤ
229 is_continuous : Bool
230
231/-! ## Summary -/
232
233/-- RS picture of phase transitions:
234
235 1. **J-cost landscape**: Multi-dimensional surface
236 2. **Minima**: Phases are local minima
237 3. **First order**: Jump between separated minima
238 4. **Second order**: Minima merge, fluctuations diverge
239 5. **Critical point**: Topology change
240 6. **Nucleation**: Thermal crossing of barriers -/