Comparison modulo a set

We study when comparison of ambient forms modulo A is decided by the maintenance–proviso test (Promain.Test). A set is Promain when the test entirely characterises comparison. We split this into the two respective directions, since each can be meaningful on its own:

• Promain.Necessary, when comparison implies the test; and
• Promain.Sufficient, when the test implies comparison.

Strikingly, sufficiency needs only that A is Form.Hereditary. Necessity, however, is the more complicated of the two: it holds when A is Downlinking, a property guaranteed for dicotically closed sets containing a root, and in particular for every Universe.

Note that we are providing sufficient conditions for Promain.Necessary and Promain.Sufficient; it remains unclear what structure can be inferred about a set A that has either of these two properties.

The main result of this section is Promain.of_dicotic_of_nonempty, which states that every nonempty, hereditary, dicotically closed set is promain.

References

• A. N. Siegel, On the general dead-ending universe of partizan games (Section 5 on pp. 207–222)

The maintenance–proviso test

def Form.Promain.Test {G : Type (u + 1)} [Form G] (A : G → Prop) (g h : G) : Prop

The maintenance–proviso test for g and h modulo A, simply requiring both the maintenance and the proviso to be satisfied.

Equations

• Form.Promain.Test A g h = (Form.Maintenance A g h Player.right ∧ Form.Maintenance A g h Player.left ∧ Form.Proviso A g h Player.right ∧ Form.Proviso A h g Player.left)

def Form.Promain {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : Prop

A set A is promain (within the ambient IsAmbient) when comparison of ambient forms modulo A is decided entirely by the maintenance–proviso test (i.e. by Test).

Equations

• Form.Promain IsAmbient A = ∀ ⦃g h : G⦄, IsAmbient g → IsAmbient h → (g ≥m A h ↔ Form.Promain.Test A g h)

def Form.Promain.Necessary {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : Prop

The necessary/'forward' direction of Promain, for when comparison forces the test.

Equations

• Form.Promain.Necessary IsAmbient A = ∀ ⦃g h : G⦄, IsAmbient g → IsAmbient h → g ≥m A h → Form.Promain.Test A g h

def Form.Promain.Sufficient {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : Prop

The sufficient/'backward' direction of Promain, for when the test forces comparison.

Equations

• Form.Promain.Sufficient IsAmbient A = ∀ ⦃g h : G⦄, IsAmbient g → IsAmbient h → Form.Promain.Test A g h → g ≥m A h

theorem Form.Promain.necessary {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} (hp : Promain IsAmbient A) : Necessary IsAmbient A

theorem Form.Promain.sufficient {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} (hp : Promain IsAmbient A) : Sufficient IsAmbient A

theorem Form.Promain.mk {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} (hn : Necessary IsAmbient A) (hs : Sufficient IsAmbient A) : Promain IsAmbient A

theorem Form.Promain.iff_necessary_and_sufficient {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} : Promain IsAmbient A ↔ Necessary IsAmbient A ∧ Sufficient IsAmbient A

Separating and downlinking sets

class Form.Separating {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) : Prop

A set A is separating (within the ambient IsAmbient) when incomparable ambient forms are separated from both sides. This is essentially Siegel, Lemma 5.8 extracted into a property.

• separating_pair_of_not_misereGE {g h : G} : IsAmbient g → IsAmbient h → ¬g ≥m A h → AreLeftSeparating A g h ∧ AreRightSeparating A g h

  If g ≱ h modulo A, then g and h are both Left- and Right-separating.

class Form.Downlinking {G : Type (u + 1)} [Form G] (IsAmbient A : G → Prop) extends Form.Hereditary IsAmbient : Prop

A set A is downlinking (within the ambient IsAmbient) when we can conclude two ambient forms are downlinked in the following way: if no Left option of g is better than h, and g is better than no Right option of h, then g is downlinked to h. This is essentially an extraction of Siegel, Lemma 5.10

This is currently the crux of proving a set is Promain.Necessary (see Promain.Necessary.of_downlinking).

• has_option {g g' : G} (h1 : IsAmbient g) (h2 : IsOption g' g) : IsAmbient g'
• downlinked_of_not_exists_moves_misereGE {g h : G} : IsAmbient g → IsAmbient h → (¬∃ gl ∈ moves Player.left g, gl ≥m A h) → (¬∃ hr ∈ moves Player.right h, g ≥m A hr) → Downlinked A g h

Currently, the auxiliary separating and downlinking forms used in our proofs are all grown dicotically from rooted adjoints with a fixed root, so they live in any dicotically closed A containing a root.

@[irreducible]

theorem Form.rootedAdjoint_mem_of_isAmbient {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] {r : G} (h_root : A r) (h_sub : A ≤ IsAmbient) {g : G} (hg : IsAmbient g) : A (rootedAdjoint r g)

The rooted adjoint of an ambient form lies in any dicotically closed A containing the root r.

theorem Form.Downlinked.of_separating {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] {r : G} (h_root : A r) (h_isRoot : Misere.Adjoint.IsRoot IsAmbient r) (h_sub : A ≤ IsAmbient) {g h : G} (hg : IsAmbient g) (hh : IsAmbient h) (h_left_sep : ∀ (gl : ↑(moves Player.left g)), AreLeftSeparating A (↑gl) h) (h_right_sep : ∀ (hr : ↑(moves Player.right h)), AreRightSeparating A g ↑hr) : Downlinked A g h

If every Left option of g is separated from h, and every Right option of h from g, then g is downlinked to h.

theorem Form.Separating.pair_of_not_misereGE {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] {r : G} (h_root : A r) (h_isRoot : Misere.Adjoint.IsRoot IsAmbient r) (h_sub : A ≤ IsAmbient) {g h : G} (hg : IsAmbient g) (hh : IsAmbient h) (h_not_ge : ¬g ≥m A h) : AreLeftSeparating A g h ∧ AreRightSeparating A g h

If g ≱ h modulo A, then g and h are both Left- and Right-separating.

def Form.Separating.of_dicotic {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] {r : G} (h_root : A r) (h_isRoot : Misere.Adjoint.IsRoot IsAmbient r) (h_sub : A ≤ IsAmbient) : Separating IsAmbient A

A dicotically closed A lying in the ambient space and containing a root r (see Form.Misere.Adjoint.IsRoot) is Separating (no further closure properties required!).

Equations

• ⋯ = ⋯

def Form.Separating.of_dicotic_of_nonempty {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] [Hereditary A] (h_ne : ∃ (g : G), A g) (h_sub : A ≤ IsAmbient) : Separating IsAmbient A

A nonempty, hereditary, dicotically closed A lying in the ambient space is Separating. Note that this is strictly weaker than of_dicotic; it is mainly included for convenience.

Equations

• ⋯ = ⋯

def Form.Downlinking.of_dicotic_separating {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] {r : G} [Separating IsAmbient A] (h_root : A r) (h_isRoot : Misere.Adjoint.IsRoot IsAmbient r) (h_sub : A ≤ IsAmbient) : Downlinking IsAmbient A

A separating, dicotically closed A in the ambient space with a root is downlinking (Separating supplies what the downlink construction needs).

Equations

• ⋯ = ⋯

def Form.Downlinking.of_dicotic {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] {r : G} (h_root : A r) (h_isRoot : Misere.Adjoint.IsRoot IsAmbient r) (h_sub : A ≤ IsAmbient) : Downlinking IsAmbient A

A dicotically closed A lying in the ambient space and containing a root r (see Form.Misere.Adjoint.IsRoot) is Downlinking (no further closure properties required!). Taking r = 0 recovers the usual case where A contains 0.

Equations

• ⋯ = ⋯

def Form.Downlinking.of_dicotic_of_nonempty {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] [Hereditary A] (h_ne : ∃ (g : G), A g) (h_sub : A ≤ IsAmbient) : Downlinking IsAmbient A

A nonempty, hereditary, dicotically closed A lying in the ambient space is Downlinking. The zero-like form it must contain (Form.exists_isZeroLike) serves as the required root.

Equations

• ⋯ = ⋯

Necessity

theorem Form.not_downlinked_left_option_of_misereGE {G : Type (u + 1)} [Form G] {A : G → Prop} {g h hl : G} (hge : g ≥m A h) (hhl : hl ∈ moves Player.left h) : ¬Downlinked A g hl

Comparison forbids downlinking to options: if g ≥m A h, then g is not downlinked to any Left option of h.

This is contrapositive of (i) => (ii) in Siegel (Proof of Lemma 5.10 on p. 215)

theorem Form.not_downlinked_right_option_of_misereGE {G : Type (u + 1)} [Form G] {A : G → Prop} {g h gr : G} (hge : g ≥m A h) (hgr : gr ∈ moves Player.right g) : ¬Downlinked A gr h

Comparison forbids downlinking to options: if g ≥m A h, then no Right option of g is downlinked to h.

This is contrapositive of (i) => (ii) in Siegel (Proof of Lemma 5.10 on p. 215)

theorem Form.Promain.Necessary.of_downlinking {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Downlinking IsAmbient A] : Necessary IsAmbient A

If A is downlinking, then comparison forces the maintenance–proviso test; i.e. Test is necessary for comparison.

theorem Form.Promain.Necessary.of_dicotic {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] {r : G} (h_root : A r) (h_isRoot : Misere.Adjoint.IsRoot IsAmbient r) (h_sub : A ≤ IsAmbient) : Necessary IsAmbient A

A concrete sufficient condition for necessity: a dicotically closed set in the ambient space containing a root.

theorem Form.Promain.Necessary.of_dicotic_of_nonempty {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] [Hereditary A] (h_ne : ∃ (g : G), A g) (h_sub : A ≤ IsAmbient) : Necessary IsAmbient A

A nonempty, hereditary, dicotically closed set in the ambient space has the necessity direction.

Sufficiency

theorem Form.Promain.Sufficient.of_hereditary {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Hereditary A] : Sufficient IsAmbient A

If A is hereditary, then the maintenance–proviso test (Test) is sufficient for comparison.

Comparison

theorem Form.Promain.of_downlinking_of_hereditary {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Downlinking IsAmbient A] [Hereditary A] : Promain IsAmbient A

If A is downlinking and hereditary, comparison modulo A is characterised by the maintenance–proviso test.

theorem Form.Promain.of_dicotic_of_nonempty {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [ClosedUnderDicotic IsAmbient A] [Hereditary A] (h_ne : ∃ (g : G), A g) (h_sub : A ≤ IsAmbient) : Promain IsAmbient A

A nonempty, hereditary, dicotically closed set in the ambient space is promain.

instance Form.instSeparatingUniverse {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [Universe IsAmbient A] : Separating IsAmbient A

Every universe is separating.

instance Form.instDownlinkingUniverse {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [Universe IsAmbient A] : Downlinking IsAmbient A

Every universe is downlinking.

theorem Form.Promain.of_universe {G : Type (u + 1)} [Form G] {IsAmbient A : G → Prop} [Ambient IsAmbient] [Universe IsAmbient A] : Promain IsAmbient A

Comparison modulo a universe is characterised by the maintenance–proviso test (Test).

Maintenance under refinement

theorem Form.Maintenance.of_subset {G : Type (u + 1)} [Form G] {A B : G → Prop} (h_subset : ∀ (g : G), B g → A g) {g h : G} {p : Player} (h_maintenance : Maintenance A g h p) : Maintenance B g h p

If B is a subset of A, then any pair of games passing the A-maintenance necessarily also passes the B-maintenance.