Computable phase boundaries and equilibrium observables
For finitely specified one-parameter local-Hamiltonian families, identify restrictions giving terminating algorithms for phase-boundary locations to rational accuracy , or for specified local order parameters. Fix the phase diagnostic, the param
Problem statement
For finitely specified one-parameter local-Hamiltonian families, identify restrictions giving terminating algorithms for phase-boundary locations to rational accuracy , or for specified local order parameters. Fix the phase diagnostic, the parameter representation and the boundary/state-selection convention; these are distinct computational tasks.
Lean 4
No Lean statement or proof is attached yet. Have a formalization? Share its source to add it to this problem.
Background
A phase diagram is not defined computationally until its phases and output representation are specified. Finite descriptions of computable coupling functions do not imply an effective convergence rate for the thermodynamic limit.
What is known: Bausch–Cubitt–Watson construct a continuous one-parameter translation-invariant two-dimensional family whose phase membership is undecidable. The conclusion is algorithmic, not that there are “uncomputably many” transitions. Purcell–Li–Cubitt's Chaitin-phase-transition preprint goes further in another direction: even a promised single transition can have an uncomputable location, Chaitin's constant. Simple topology of the diagram is therefore insufficient.
There is an important positive result with different quantifiers. Fawzi–Fawzi–Scalet's certified equilibrium-state hierarchy decides the promised threshold question when every translation-invariant equilibrium state has its observable expectation on the same side of the separated thresholds. This does not compute the expectation selected by arbitrary boundary conditions, nor supply every phase boundary or both exact endpoints of an equilibrium-expectation interval. The frontier must distinguish all equilibrium states from a selected thermodynamic-limit state. Related: U1, U3, B10.
Progress & source assessment
Source catalogue review: 4 September 2026. Improved indicates partial progress, including qualified preprint claims.
preprint: A single phase transition at an uncomputable location; a finite number of transitions does not ensure computability. Evidence
published: Certified equilibrium-observable bounds and a terminating separated-threshold promise problem with quantification over all translation-invariant equilibrium states. Evidence
Recorded progress
Add yours →Nothing recorded yet. A pointer to a paper the entry is missing counts.
Machine attempts
0 recordedAttempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.
No machine attempts recorded.
Sign in to run an attempt. New accounts start with enough credits for ten.
Discussion
0 notesNotes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.
No notes yet.
Sign in to add a note.