TopologicalTransition
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.