Subadditivity, contraction-map soundness and monogamy of mutual information for the holographic graph model, kernel-checked in Lean 4

Last updated 2026-10-20

IRSI (irsi.ai). Code and data: moon-holo-lean-bundle.zip (this note, the Lean sources, the replay tool and the recorded axiom and replay output). The helper scripts under tools/ named in the text are not in the bundle.

Scope and limits (read first)

• This is a formalization of known mathematics (contraction maps: Bao et al., arXiv:1505.07839; soundness theorem: Bao and Naskar, arXiv:2403.13283, Theorem 1; the explicit MMI map: Bao, Furuya and Naskar, arXiv:2409.17317, Section 3.2). It certifies no new entropy inequality. Earlier sorry-free Lean proofs of graph-model entropy, subadditivity, monogamy of mutual information and unit-coefficient contraction-map soundness exist in paulklemstine/Lean (https://github.com/paulklemstine/Lean, Catalog/Novelty/, commit d3021737, 2026-08-16; see Related work), so we claim no priority for the graph model, SA, MMI or the soundness theorem in its unit-coefficient form. What this note adds, as far as we could find in that directory, is (i) a generic Boolean checker for contraction maps with a proved soundness theorem (checkContraction, checked_contraction_sound), applied to the MMI map by decide, and (ii) soundness with real non-negative coefficients α, β on the two sides of the inequality (contraction_sound), whose all-ones case has the same form as their unit-coefficient statement (in our weighted-graph setting rather than theirs). Both are small variations on their approach, not new mathematics.
• Proved for the finite weighted-graph min-cut model only, not for continuum RT/HRT. The theorem is stated for pairwise disjoint regions (see the MMI row). This is the form in which MMI is stated in the literature (Hayden, Headrick and Maloney, arXiv:1107.2940, arbitrary disjoint regions A, B, C), so it is not a weakened special case; for overlapping regions the inequality is false in general (one unit edge between two boundary vertices with A = B = C = one endpoint gives 4 ≤ 3), and we do not prove any other form.
• No inequality involving four or more parties (five-term and later holographic inequalities) is covered here. Only the MMI contraction map is checked. (paulklemstine/Lean proves a five-party cyclic inequality with its own contraction map; we have not formalized it.) We do not prove that a contraction map exists for any other inequality, and strong subadditivity is not a separate theorem here.
• SA is close to a definitional fact about min cuts (take the union of two optimal cut sets). It is included as the base case, not as a result.
• Review status: the statements were read by one non-physicist model reader. An expert reading is recommended. The Lean files were written by a Codex session (original build on Lean 4.33.1, 2026-10-15) and independently rebuilt on Lean 4.34.0 (pinned Mathlib) by a second model session in the same lab (2026-10-15), which ran the compile, axiom checks and the one kernel replay behind the 94-declaration record (runs/verify-replay-4.34.0.log, not shipped). No outside human review has been done. Five lab-internal adversary passes (model sessions that rebuilt the Lean files on Lean 4.34.0 in a sandbox and attacked the stated claim) were run; their reports are not shipped and are identified here by lab-internal ids: 7a39b47d and 03f99908 WEAKENED (minor, wording), e9e4e22b WEAKENED (the kill-test chronology, corrected in the Chronology item), 2aa679a9 and d63af7fd SURVIVED. Automated outside model reviews exist; they are unverified and we treat them as advice only.
• Chronology: the kill test for this project was registered with a deadline of 2026-10-15T18:00Z (criterion in the registration: sorry-free SA and the contraction lemma stated, after two Codex sessions). By the builder's own file timestamps and logs the Lean build started at about 17:09Z; the six source files were written between 17:24Z and 17:29Z, and the builder's own compile of all six files, its kernel replay of the 94 declarations and two rejected injected-bad-fixture tests ran between 17:29Z and 17:30Z, in one Codex session (not two). So the registered criterion was met by about 17:30Z, about 30 minutes before the original deadline. Timestamps are file modification times and machine-written logs; they are not signed, and the six files in the project directory carry a later copy time (18:33Z). The independent confirmation came afterwards: the second session's rebuild ran about 18:25Z to 18:46Z and the result rows were filed at 18:43Z; the independent rebuild is a requirement of the later bet file, not of the registered criterion. The lab director's note moving the deadline to 2026-10-16T18:00Z is stamped 17:12Z, before the original deadline, and a machine-written status entry at 17:25Z already shows the new deadline, so the extension was issued before the original deadline; the note's wording that the 18:00Z date had "passed" is an error. The bet file (BET.json) was frozen at 18:32:43Z, after the work (begun 17:09Z, done by about 17:30Z), so the bet was registered after the work, not before it; the only pre-build commitment is the original registration. The deadline change is recorded only in the lab's internal project log (not shipped); we know of no separate registration of it. We therefore claim technical completion by about 17:30Z by the builder's own record, followed by an independent confirmation, and we do not call it a pass of the registered test as run.
• Timestamp hygiene: the first-pass verification logs carried timestamps later than the real clock (18:50Z, 18:55Z, 18:56Z); they were corrected to the real time by editing, and no audit trail of that correction was kept. The times above should be read as approximate to a few minutes. The mathematical claims do not depend on them; they can be rechecked from the hashed sources with the build recipe below.
• The original build used Lean 4.33.1 (its Mathlib commit was not recorded). The independent rebuild used Lean 4.34.0 with Mathlib 5ed2965256430c3649e86755f9576b54eca72435. The kernel replay trusts imported Mathlib declarations and uses the deprecated Lean.Environment.replay; the recorded kernel replay was run once, by the independent session on Lean 4.34.0; it was not repeated on 4.33.1 and has not been run by anyone outside the lab. Anyone relying on the replay should rerun it with the command below.
• An outside reader cannot rerun everything from this note alone: the package has no lakefile and the replay tool is a project script. The compile commands are given below and the sources are hashed.

Abstract

We give a Lean 4 / Mathlib formalization of the finite weighted-graph (min-cut) model of holographic entropy. In it we prove subadditivity (SA), the soundness of the contraction-map proof method for arbitrary linear entropy inequalities, a reflective checker for contraction maps with a proved soundness theorem, and monogamy of mutual information (MMI) for pairwise disjoint regions in every finite graph. Sorry-free Lean proofs of the graph-model MMI and of unit-coefficient contraction-map soundness were published earlier (paulklemstine/Lean, 2026-08-16); what we add to them is the generic checker and the real-coefficient form of soundness (see Scope and limits). All theorems depend only on the standard axioms propext, Classical.choice and Quot.sound, and the compiled modules replay through the Lean kernel (one replay, run once by one session of this lab on Lean 4.34.0 with the deprecated Lean.Environment.replay; imported Mathlib declarations are trusted; see the limits below).

Setting

A finite undirected graph has vertex set V, edge set E and nonnegative real edge weights. Parallel edges and loops are allowed by the Lean definition. A set of boundary vertices is distinguished; a purifier is just one more boundary vertex, and bulk vertices are the rest. For a set A of boundary vertices, the entropy S(A) is the minimum total weight of cut edges over all vertex sets U whose intersection with the boundary is exactly A (the admissible cuts); bulk vertices may lie on either side. The Lean definitions are in lean/GraphEntropy.lean.

Exact Lean forms (WeightedGraph has fields src dst : E → V, weight : E → ℝ and a proof nonneg : ∀ e, 0 ≤ weight e; V and E are Fintype, no connectivity or simplicity is assumed):

cutWeight G U := ∑ e, if (G.src e ∈ U ↔ G.dst e ∈ U) then 0 else G.weight e
Admissible boundary A U := ∀ v ∈ boundary, (v ∈ U ↔ v ∈ A)
entropy G boundary A := cutWeight G (minCut G boundary A)   -- minCut: a chosen admissible minimizer (exists_min_cut)
theorem SA  (G) (boundary A B : Finset V) :
  entropy G boundary (A ∪ B) ≤ entropy G boundary A + entropy G boundary B
theorem MMI (G) (boundary A B C : Finset V) (hAB : Disjoint A B) (hAC : Disjoint A C) (hBC : Disjoint B C) :
  entropy G boundary A + entropy G boundary B + entropy G boundary C + entropy G boundary (A ∪ B ∪ C) ≤
  entropy G boundary (A ∪ B) + entropy G boundary (A ∪ C) + entropy G boundary (B ∪ C)

The disjointness hypotheses in MMI are on the whole vertex sets, which is stronger than disjointness of their boundary parts; entropy itself sees only A ∩ boundary.

Theorems

All in namespace Holographic, with graph G, boundary set boundary, and finite vertex sets A, B, C (only their boundary parts matter).

Full Lean forms of the remaining theorems (copied from the sources; L R are Fintype index types):

weightedDistance coeff x y := ∑ i, if x i = y i then 0 else coeff i
structure ContractionCertificate L R boundary lhs rhs alpha beta where
  map : (L → Bool) → (R → Bool)
  alpha_nonneg : ∀ i, 0 ≤ alpha i
  beta_nonneg  : ∀ j, 0 ≤ beta j
  contracts : ∀ x y, weightedDistance beta (map x) (map y) ≤ weightedDistance alpha x y
  boundary_condition : ∀ v ∈ boundary, map (fun i => decide (v ∈ lhs i)) = fun j => decide (v ∈ rhs j)

theorem contraction_sound (G : WeightedGraph V E) (boundary : Finset V)
    (lhs : L → Finset V) (rhs : R → Finset V) (alpha : L → ℝ) (beta : R → ℝ)
    (cert : ContractionCertificate L R boundary lhs rhs alpha beta) :
    ∑ j, beta j * entropy G boundary (rhs j) ≤ ∑ i, alpha i * entropy G boundary (lhs i)

def checkContraction (alpha : L → ℕ) (beta : R → ℕ) (f : (L → Bool) → (R → Bool)) : Bool :=
  decide (∀ x y, natDistance beta (f x) (f y) ≤ natDistance alpha x y)   -- needs [DecidableEq L]

theorem checked_contraction_sound (G : WeightedGraph V E) (boundary : Finset V)
    (lhs : L → Finset V) (rhs : R → Finset V) (alpha : L → ℕ) (beta : R → ℕ)
    (f : (L → Bool) → (R → Bool)) (h : checkContraction alpha beta f = true)
    (hb : ∀ v ∈ boundary, f (fun i => decide (v ∈ lhs i)) = fun j => decide (v ∈ rhs j)) :
    ∑ j, (beta j : ℝ) * entropy G boundary (rhs j) ≤ ∑ i, (alpha i : ℝ) * entropy G boundary (lhs i)

def mmiMap (x : Fin 3 → Bool) : Fin 4 → Bool :=
  ![x 0 && x 1 && !x 2, x 0 && x 2 && !x 1, x 1 && x 2 && !x 0, x 0 || x 1 || x 2]
theorem mmiMap_checked : checkContraction (fun _ : Fin 3 => 1) (fun _ : Fin 4 => 1) mmiMap = true := by decide

Not proved here: that a contraction map exists for any inequality other than MMI; strong subadditivity as a separate named theorem (it follows from SA and MMI mathematically, but that step is not formalized); any converse (completeness) statement.

Build recipe and checks

• Lean 4.34.0 with Mathlib at commit 5ed2965256430c3649e86755f9576b54eca72435 (tag v4.34.0, from lake-manifest.json).
• Six files, in dependency order: GraphEntropy, Contraction, Checker, MMI, Examples, KillTest (lean/). Compile each with lake env lean -o <name>.olean <name>.lean inside a Lake workspace that depends on Mathlib; all six exit 0. The only warning is a deprecated import (Mathlib.Data.Real.Basic).
• Source SHA-256: GraphEntropy 8011e236a02b8a30a46e7f981c85c293b86368a8ee7a68f5cfd35a6c79e3c900; Contraction 67511df797ab01c1a672f30c038db8a3ad6c3548b27c70bd70f71accd52d65cb; Checker a6fe842b4dd7143320b504c60254bf34ca9cf2d1d5770e89e8da1a5748f00b94; MMI b282ad86ad27cce4384ce9d9f38f7c6d9ba5aa670656c1101f3a6515e22ad65f; Examples dae2b162fd4e8fed21fe13d4f7f42b9aa418a23d063c5a875a0c51ce296e3e45; KillTest f1e4fcbff3d9ada6328040b9122e3020ac917287838cf09a791c218e2a54675b; lean/tools/Replay.lean 5eb2a94e418b436c1ae74ef4be424cb440a652045f31831085f966aa68f487de.
• Axioms: #print axioms for SA, exists_min_cut, contraction_sound, checkContraction_sound, checked_contraction_sound, mmiMap_checked, MMI and the example theorem Examples.star_entropy_three each list exactly [propext, Classical.choice, Quot.sound] (runs-public/axioms-and-replay.txt).
• Kernel replay (a LeanChecker-style re-check of every compiled declaration in a fresh environment, lean/tools/Replay.lean): OK for all six modules, 53 / 13 / 11 / 3 / 14 / 0 declarations (94 in total: GraphEntropy, Contraction, Checker, MMI, Examples, KillTest), no project axioms or placeholders. Imported Mathlib declarations are trusted. Command (after compiling the six modules into one search path): lake env lean -j1 -s8192 --run lean/tools/Replay.lean GraphEntropy Contraction Checker MMI Examples KillTest (the logged invocation, run from the directory holding the .olean files); it prints REPLAY OK <module>: <n> declarations per module. Mapping from the theorems above: SA and exists_min_cut are in GraphEntropy, contraction_sound in Contraction, checkContraction_sound, checked_contraction_sound and mmiMap_checked in Checker, MMI in MMI, Examples.star_entropy_three in Examples.
• Source grep for sorry, admit, native_decide, axiom, unsafe, implemented_by, extern, opaque, set_option, elab, macro, run_cmd, initialize: matches only the #print axioms lines in the library files; lean/tools/Replay.lean (not part of the proof) uses unsafe and axiomInfo to implement the replay.
• Finite sanity enumeration (not evidence for the theorems; the theorems hold by proof). Script tools/sanity_enum.py, output runs-public/sanity_enum.out, written by the author of this note and run in a sandbox. (a) All 729 graphs on 4 boundary vertices with 6 edges of weight in {0,1,2} and no bulk vertex: SA holds for all 186,624 ordered pairs and MMI for all 43,740 nonempty pairwise disjoint triples; the MMI slack is exactly 0 in every case, so this family cannot distinguish MMI from equality. (b) All 59,049 graphs with 4 boundary vertices, 1 bulk vertex and 10 edges of weight in {0,1,2}: SA holds for 15,116,544 pairs and MMI for 3,542,940 triples, with MMI slack up to 4 (positive in 11,664 graphs). (c) Control: the unit-weight star with four leaves (A, B, C and the purifier O) around one bulk vertex has MMI left side 4 and right side 6. An earlier internal figure of 455,625 checks came from a script that we could not reproduce under any natural reading and is not used.

Related work

MMI for holographic entropy (RT, and hence graph min-cuts) was first proved by Hayden, Headrick and Maloney (arXiv:1107.2940, Phys. Rev. D 87, 046003); the graph-model setting of the holographic entropy cone is developed in Avis and Hernández-Cuenca (arXiv:2102.07535). Contraction maps are due to Bao et al. (arXiv:1505.07839). Bao and Naskar (arXiv:2403.13283, Theorem 1) prove the soundness of the contraction method on paper, and Bao, Furuya and Naskar (arXiv:2409.17317, Section 3.2, Table 1) give an explicit MMI contraction map; they (arXiv:2506.18086) also show that contraction maps are necessary as well as sufficient for rational linear inequalities. The Python toolkit c0mpli/hecate includes a contraction-map checker, and sergiohc95/holographic-entropy-cone stores contraction certificates and graph realizations; neither is kernel-checked. The repository kaplan196883/QIQT-H reports Lean results on cut-capacity purity and subadditivity (we read cut_compl and cut_union_le in lean/mathlib/QIQTH/EmergentSpacetime.lean: symmetry of the cut capacity under complement and subadditivity of the cut-capacity functional for nonnegative weights; we did not check that the whole repository builds), and we have not found there entropy defined as a minimum over admissible cuts, contraction soundness or MMI. The Lean repository jagg-ix/catept-main contains, in CATEPTMain/Integration/AdSCFTHeadrick1907Bridge.lean (commit 01f70e0e), theorems rtEntropy_ssa_of_area_ssa and rtEntropy_mmi_of_area_mmi; as we read the file, their hypotheses are the area-level inequalities and the proofs rescale them by 1/(4 G_N), so they do not model graph min-cuts. We did not check that the repository builds. Lean-Quantum (arXiv:2607.05492) formalizes the sandwiched Renyi data-processing inequality, a different setting (quantum states, not graph min-cuts). Flow/min-cut theory exists in Isabelle (AFP Flow_Networks), and in Lean in the CLRS-Lean project (tanktechnology.github.io/CLRS-Lean, Section 24.6, theorem Flow.maximal_iff_exists_cut_value_eq; we read the page and did not check that the development is free of sorry); this work defines entropy as an admissible-cut minimum directly. Holographic entropy cone background and recent work on its characterization and combinatorics: Grimaldi, Headrick and Hubeny (arXiv:2508.21823, SciPost Phys. 20, 122) and Grimaldi, Headrick, Hubeny and Shteyner (arXiv:2601.09987); we have not checked whether they prove MMI for overlapping subsets in a form we could cite. The state of the N=6 extreme-ray problem is in He, Hubeny and Rota (arXiv:2412.15364) and He, Lee and Ooguri (arXiv:2601.19979, which attacks the six rays of 2412.15364 without a known graph model; we have not checked how they relate to our 13). Earlier Lean proofs of the same core results exist. The repository paulklemstine/Lean contains, in Catalog/Novelty/ and in a single commit d3021737 dated 2026-08-16T18:47:46Z by the GitHub per-file commit history (committer dates can be set by the author; about two months before our build), three files that we read in full: EmergentGeometryEntropyCone.lean (399 lines: a finite graph with real symmetric non-negative weights, entropy as a minimum over admissible bulk regions, entropy_subadditive, entropy_strong_subadditive, entropy_monogamy for pairwise disjoint regions, exists_minimal_surface), HolographicContractionCalculus.lean (153 lines: a structure ContractionMap k m of Hamming-distance-non-increasing Boolean maps, entropy_le_of_contraction, which is unit-coefficient contraction soundness, minorityMap, which is the same Boolean map as our mmiMap, and mmi_of_contraction) and HolographicCyclicInequality.lean (194 lines: entropy_cyclic5, a five-party cyclic inequality, with its contraction map cyclicMap). The files contain no sorry, admit, axiom or native_decide, and on 2026-10-20 we compiled them unmodified with Lean 4.34.0 and the Mathlib used here: all three exit 0 with no warnings, and #print axioms for entropy_monogamy, entropy_subadditive, entropy_strong_subadditive, entropy_le_of_contraction, mmi_of_contraction and entropy_cyclic5 lists only [propext, Classical.choice, Quot.sound] (runs-public/klemstine-compile-check.txt; we did not run the kernel replay on their files). We did not search the rest of that repository, which also holds related files (for example EmergentGeometryObstructions.lean and CyclicIndependence.lean) that we did not read in detail. We learned of the repository from our own literature sweep on 2026-10-20; our searches of 2026-10-15 and 2026-10-19 (arXiv, GitHub, Zenodo, and a web search for Physlib, the merged PhysLean / Lean-QuantumInfo library; the Lean Zulip, OpenReview and the Physlib repository itself were not searched) did not find it. Compared with those three files, we found in Catalog/Novelty/ (a grep at HEAD 990ac235, 2026-10-20, of the 991 .lean files of our sparse, shallow clone, which holds only Catalog/Novelty/ of the repository's 28,227 .lean files; a GitHub code search of the default branch the same day for checkContraction, checked_contraction_sound, weightedDistance and ContractionCertificate also returned nothing; other branches were not searched) no Boolean checker for arbitrary contraction maps with a soundness theorem (their instances are closed by a lemma per inequality, sepBit_mmi, sepBit_cyclic5, each by decide over the Boolean arguments), and no coefficients α, β in the soundness theorem. Earlier Lean work on graph-cut subadditivity also exists in the QIQT-H item above.

Side result: tree models of N=6 extreme rays (not a Lean result)

This section is separate from the formalization above, is computer-assisted (exact integer arithmetic in Python, no Lean), and is not part of the proofs.

• Data: the 4,161 stored N=6 graphs found in our clone of sergiohc95/holographic-entropy-cone (commit 36ff9c38c1a08e93222a327951c5d82c93e6c990, directory data/n=6, cloned 2026-10-15; sha256 of data/n=6/rays.json ad529468d8bfa748a88389c0113854f82b10d76997c3a103ec812e2ecf78a1ea and of graphs.json 2d09da4fec8710d3a2b21f73825cb4d0ffe7374c30ffab8022b80b3cfa9c2b98; the ray indices below are positions in that clone's list, not stable upstream identifiers). The repository's current README lists a much larger N=6 set (387,359 ray representatives, catalogue marked partial), so the ray indices are valid only for that commit. We recomputed all their entropy vectors (purifier included) and matched the stored rays up to scale (0 mismatches; data/n6-repro.json). Of the 4,161 stored graphs, 329 contain bulk cycles; we studied the 13 of them in the last 208 list positions (indices 3953 to 4160, the 'tail', which we guessed from the list order to be the part holding the hardest rays; this guess is not confirmed). Ray 3933 is also bulk-cyclic but lies outside that range and was not studied. Elsewhere in this note 'the 13 rays' means these 13 (3984, 4040, 4069, 4075, 4077, 4080, 4086, 4141, 4147, 4151, 4152, 4156, 4160).
• Question: which of those 13 rays also have a model whose bulk is a tree after splitting each boundary vertex into several leaves ("tree-after-splitting"). Search by an alternating-LP heuristic, then exact check of all 63 region entropies (tools/tree_verify.py, plus an independent reimplementation tools/tree_verify_indep.py).
• Result: all 13 rays (indices 3984, 4040, 4069, 4075, 4077, 4080, 4086, 4141, 4147, 4151, 4152, 4156, 4160) have exact tree-after-splitting models with integer weights (data/tree-models/, 16 model files, since 3984, 4086 and 4156 have two models each; five bulk nodes for eleven of the rays, six for 4077 and 4141). Twelve were found earlier; the last one, 4141, was found on 2026-10-20 (see below). The repository's own stored graph for 4141 has a bulk cycle; what our search adds is a model whose bulk is a tree, not the realizability of the ray. Each model was checked in exact integer arithmetic over all 63 regions by tools/tree_verify.py (vector equals the ray with scale 1) and, for 4040, 4151, 4152 and 4141, also by the separately written tools/tree_verify_indep.py, which also checks purity (the model for 4141 has 13 vertices: 7 boundary and 6 bulk; 5 bulk edges with weights 1, 1, 2, 2, 1; nonnegative weights). Ray 4141 first had no model on any of the path, star and fork skeletons with at most 5 bulk nodes in the class below: the certified search (exact Farkas certificates replayed in integer arithmetic, data/tree-cert/) ended with 0 open leaves on all three and two separately written checkers accepted those certificates (one rejected 95 of 96 tampered copies; the remaining edit is still a valid certificate). The heuristic search had found no model for 4141 with up to 6 bulk nodes, which proved nothing, and two serial, time-budgeted rounds of the certified search over the six-vertex bulk trees (6000 s and 6600 s per tree) ended with open leaves and no model. A third round split the open leaves of those exact proof trees over parallel processes (a splitting script, tree_cert_split.py, not shipped; one rented CPU box, 56 minutes); each merged proof tree was replayed exactly. For the six-vertex star t6b the search closed with 0 open leaves and a negative (status infeasible, replay exact), and for the tree t6f (a bulk edge joining two bulk nodes of degree three, each with two leaf neighbours) it returned a model. We stopped the box at that point, so the other four six-vertex trees were not finished and no claim is made about them (their searches were incomplete, not negative). The model for 4141 is data/tree-models/r4141-t6f.json; it was extracted from the model event of the t6f proof tree (which tree_cert.py re-checks in exact arithmetic when replaying) and then verified by the two verifiers above. The certificate file is large and is not in data/. The certified class for the negatives is: bulk forest on at most 5 vertices (path, star, fork; for 4141 additionally the six-vertex star t6b alone), split boundary leaves, no direct boundary-to-boundary edges, edge weights capped at the largest entry of the ray; the reduction steps behind the search (normalization, symmetry, skeleton coverage) are paper arguments with random tests, not Lean proofs. The positive result for 4141 does not rely on them: it needs only the exact check of the model, whose bulk is a tree and whose boundary parties appear as several leaves.
• The 13 rays come from the repository's data, which presents them as holographic; we did not re-derive that. The finding concerns only the existence of a tree model, for 13 rays of one dataset snapshot.
• Orbit check against arXiv:2412.15364 (2026-10-20; tools/orbit_match.py, tools/sac_rank.py, notes and outputs in data/orbit/, exact integer arithmetic, our own code, no independent reimplementation). We took the list of 208 extreme-ray orbits from the Rota repository (Max-Rota/SSA-compatible-Extreme-Rays-of-the-Subadditivity-Cone, n=6/rays.txt, sha256 4e39168b0d21e1723e98ea3c9c4f08b4c90c573519b47db257baab5079833344, line k read as ER#k; commit not recorded) and compared up to permutations of the six parties and the purifier and up to scale. Result: none of our 13 stored rays, including 4141, is in any of the 208 orbits. The reason we found is that none of the 13 is an extreme ray of the subadditivity cone: the tight subadditivity and Araki-Lieb instances at each of them have rank 40 to 55, while an extreme ray needs rank 62 and all 208 listed vectors have rank 62. So the 13 lie outside the paper's enumeration, which is of subadditivity-cone rays; they are not candidates for its open orbits. Controls: the 208 orbits are pairwise distinct, and 131 of them do occur among the 4,161 stored rays, so the matcher finds matches when they exist. Orbit #111 is the orbit of stored ray 293, whose stored graph has a bulk cycle on four bulk nodes; orbit #207 does not occur among the stored rays. A heuristic search (tools/tree_ls.py, path, star, fork and five six-node skeletons, up to 3,000 restarts) found no tree model for #111 or #207; that proves nothing, and we ran no certified search. Nothing here is a statement about the six orbits without a known graph model or about the whole N=6 cone.
• A tree with several boundary leaves standing for one party is not a simple tree graph model; results for simple trees (arXiv:2512.24490, 2512.18702) do not apply to our tree-after-splitting class without a separate argument.

Outlook

With models now found for all 13 stored rays, the questions below are suggestions of ours; we have no evidence of anyone's current priorities and do not predict what the named researchers will do. The outcome for 4141 changed on 2026-10-20 (a model with six bulk nodes), so the earlier remark that it was the only ray without a tree-after-splitting model no longer holds.

• Authors of arXiv:2412.15364 (He, Hubeny and Rota). What they can do now that they could not before is limited, and the 13-of-13 result does not touch their open cases. (1) They can take as settled that our 13 stored bulk-cyclic rays are not among their 208 orbits and see why (rank 40 to 55 against 62), so those 13 are examples of extreme rays of the holographic cone, in the dataset's reading, that a subadditivity-cone enumeration does not list and that nevertheless have tree-after-splitting models with five or six bulk nodes (data/tree-models/). (2) For their orbit #111 they can use the match to stored ray 293, whose stored graph has a four-node bulk cycle, as a ready entry point: data/orbit/ holds the inputs, the canonical-form matcher and the exact rank test, so a candidate tree model for #111 or #207 can be checked against the ray and its orbit with tools/tree_verify.py and the same files. (3) The search tools (tools/tree_ls.py, tools/tree_cert.py) are the ones that produced the 13 models; we ran them on #111 and #207 only as a heuristic and found nothing, so whether either orbit has a tree model is still open. We do not know whether they want any of this.
• Holographic-entropy-cone researchers (Hernández-Cuenca, Hubeny, Rota; the contraction-map group of Bao, Furuya and Naskar): because all 13 rays have tree-after-splitting models, they are no longer candidates for a tree-realizability test. The chordality results (arXiv:2512.24490, 2512.18702) are for simple trees and would first need an argument covering split boundary leaves; whether our models are of interest for that is for them to say.
• He, Lee and Ooguri (arXiv:2601.19979) used reinforcement learning on the six rays of 2412.15364 that had no known graph model and, by their abstract, realized three and gave evidence of non-existence for the other three. An unreviewed third-party repository (afletc-a11y/holographic-mystery-rays) claims realizations for three further rays (110, 145, 168); its README says that Temple He and collaborators had already established these in earlier unpublished work and then checked the graphs in Mathematica, and the repository claims no priority; we have not checked its graphs, and as we read the paper those six are among its 208 orbits, so by the orbit check above none of our 13 stored rays is one of them.
• Our searches covered only the 13 stored rays named above in one dataset snapshot; the four unfinished six-vertex trees for 4141 are not needed for the result.

Reproducing the side result

tools/tree_ls.py (heuristic), tools/tree_cert.py (certified search and certificate replay), tools/tree_to_graph.py, tools/tree_verify.py, tools/tree_verify_indep.py; models in data/tree-models/; summary and dated updates in data/tree-search.md.