Infinitely branching.
Every branch ends.
In the Aubone–Iovino model existence game, infinitary inconsistency produces finite commitments that no structure satisfies.
Infinitely branching. Every branch ends.
The theory T01 axiomatizes the Hilbert-space and lattice structure together with a {0,1}-valued probability measure. It has no model, although every finite subset of its axioms has one. Olivia’s winning strategy yields a well-founded tree: Josh’s countable answers produce infinite branching, but every play ends at a finite position satisfied in no structure.
Follow one of Josh’s answers to its terminal position. The drawing is schematic; the displayed lengths do not claim that a uniform bound is impossible.
Only finitely many answers are drawn; the omitted choices continue over the natural numbers. A terminal position is an unsatisfiable finite set of commitments, not an inconsistent finite subset of the axioms. The existence of a winning strategy with a uniform finite bound on play length remains open.
Follow a play.
Answer for Josh. This guided schematic follows the strategy used in the paper. Choose a finite cutoff and a high-probability basis ray; the later commitments locate the contradiction in a four-dimensional block.
A leaf keeps its dependencies.
One leaf, opened up. Each commitment of the final position is shown with what forced it: the countable answer, the instances of the axioms, the geometric identifications and the interval commitments, down to one basic sentence that has received intervals with no common point. Hover over a node to light up everything it depends on. The parity count is one bracketed module of this derivation.
Here μ is the probability predicate, κᵢ extracts a sequence entry, at(x) names the ray of a nonzero vector x, and spa(s) names the span of a sequence. For a basis B = (v₀, …, v₃), the sequence s_B has entries v₀/16, …, v₃/16 followed by zeros. The diagram compresses the required axiom instances, including the measure-additivity step from the high-probability atom to its block.
The parity module.
In plays that reach every commitment required by the parity argument, the terminal commitments concern nine bases of four rays inside the selected block, in the configuration of Cabello, Estebaranz and García-Alcaine. The leaf records each ray once in each of its two bases, together with an explicit identification derived from axioms that do not mention the measure. Choose a ray and omit its identification: the remaining constraints become satisfiable, so the contradiction uses every one of the eighteen.
All nine bases and eighteen identifications
The count tolerates error. If each value lies within δ of 0 or 1 and each basis sum lies within η of 1, it still refutes the commitments whenever 4δ + η < 1, and this holds for the ordinary ray presentation as well. What the leaf adds is where the intervals come from: they are Josh's explicit commitments, each with the challenge that forced it.
The same separation of occurrences and identifications holds for the 49-ray set found by our search: detaching any one of the 92 occurrences of a shared ray makes the remaining basis-and-identification constraints satisfiable.
The 49-ray configuration.
The search configuration has 36 bases and 108 contextual occurrences. Its 33 shared rays account for 92 occurrences. Detach one occurrence to inspect an assignment that satisfies every basis constraint and every remaining same-ray identification.
Filled entries have value 1; the other entries have value 0. The pink outline selects the occurrence. This check concerns the displayed basis-and-identification constraints; it does not assert minimality under all orthogonal-pair constraints. The nine-basis parity count does not apply to this configuration.