Time monotonicity of a freezing process on finite graphs: the sharpness of θ* and the θ* slice — confirmed statements and open questions of the sprints LANFORD and KELVIN
Abstract
Abstract. On a finite simple graph consider the freezing process: every directed edge carries a clock of rate one, and when it rings, the state of its head is flipped if its tail is occupied. We ask whether S_G(θ,t) = Σ_j E_{e_j}[θ^{|v_t|}], started from the configurations with a single occupied vertex, is non-increasing in the time t. The background is the landmark (M) on the late-time decrease of the limit density of the earlier model (θ ∈ [3/10, θ*], θ* = √2 − 1). The confirmed statements are 8 from LANFORD (theorems 6, open-question forms 2) and 14 from KELVIN (lemmas 4, theorems 9, open-question form 1). (i) The sharpness of θ*: the set of θ ∈ (0,1) for which S_G(θ,·) is non-increasing on every connected graph is contained in (0, θ*] (for θ ∈ (θ*, 1), S increases at late times on the paw, a triangle with a pendant vertex — LANFORD 1-2). On every connected graph with at most 6 vertices S is non-increasing for every θ ∈ (0, θ*], and over all connected graphs with 4 to 6 vertices the set of θ ∈ (0,1) with this property is exactly (0, θ*] — θ* is the threshold within this range (1-3, together with 1-2). On the other hand, on a certain graph with 8 vertices S increases at late times for θ ∈ [1/20, 2/5] (1-5), so the statement "non-increasing on every connected graph for every θ ∈ (0, θ*]" is false. (ii) The θ* slice (T1) — S_G(θ*,·) non-increasing on every finite connected graph — is equivalent to the expected number of particles of the double-flipping process (DFP) at the θ* rates, started from the empty configuration, being non-decreasing (KELVIN 1-1; a direct consequence of a known construction), and it is neither proved nor refuted (KELVIN 1-6). The closed parts are: at most 6 vertices, complete graphs, stars. (iii) Maps of the rate plane and of families, counterexamples to stronger forms, a chain of sufficient conditions together with the fact that its entrance premises fail as premises holding on all finite connected graphs (each of them fails on at least one of the lollipops with 10, 13 and 14 vertices), and obstructions to proof forms are confirmed. There were 3 proof-review rounds in LANFORD and 4 in KELVIN (each round by a fresh, context-free AI instance; Section 5). No novelty is claimed; the relation to known results is in Section 3. Version note. v1.0 (2026-09-27): public version of the note. The note is an index of the confirmed statements of the sprints LANFORD (8 confirmed) and KELVIN (14 confirmed); it contains no new claim and no proof — the proofs are in the Japanese canonical volumes attached to this record. Proof reviews: 3 rounds in LANFORD and 4 in KELVIN. The note itself had one manuscript review (r5, conditionally accepted with 3 mandatory fixes) and one narrow re-review (r6, accepted with no mandatory fix); neither is a proof review. Each review was done by a fresh, context-free AI instance (Section 5 of the note). The record holds: the note in English (PDF) and its Japanese canonical text (Markdown); the Japanese canonical volumes of KELVIN (4) and LANFORD (3); the claim ledgers and the errata of both sprints, and the KELVIN relation table to known results; the KELVIN certification tools with their records, run logs and the KELVIN files they depend on (one zip file; kv_cert_05.py also needs the LANFORD repository at commit c036d6d); the final handover documents (KELVIN v2 and v1, LANFORD); and the decision logs and the intervention logs of both sprints (the LANFORD files are copied from its repository at a fixed commit, the decision logs byte for byte from the progress ledgers). The eighth work of a series after Phase R (10.5281/zenodo.21979354), Project LOSCHMIDT (10.5281/zenodo.22233373), Project ZERMELO (10.5281/zenodo.22313877), Project STOSSZAHL (10.5281/zenodo.22437728), Project EHRENFEST (10.5281/zenodo.22734680) and Project KAC (10.5281/zenodo.22864567); the seventh, Project LANFORD, is included in this note.
// Source
Authors: Yukie Maeda