Finite descent outside a closed family

Proved

OPG500Counterexample.finite_good_outside

by hao jia · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsformalizationgeodesicsgraph-theory

Let $C$ be a type of objects with a complete finite list, a weak total preorder $\preceq$ , and a strict relation $\prec$ compatible in the sense that $a\preceq b$ rules out $b\prec a$ . Let each object have a code in a type $V$ with a binary combination, and let $I\subseteq V$ be closed under that combination.

Assume every object that is not good splits into two strictly smaller objects and that its code is the combination of their codes. If at least one object's code lies outside $I$ , then

\exists c,\quad c\text{ is good and }\operatorname{code}(c)\notin I.

The finite list must contain every object; duplicates and ties are allowed.

Preamble

import Definitions.Def_opg500_weighted_cycle_models

Formal statement

namespace OPG500Counterexample

universe u v

/-- A complete finite table supplies a minimal good object outside any predicate
closed under the binary combination, provided every nongood object splits into
strictly smaller children and weak comparison excludes strict descent. -/
theorem finite_good_outside
    {C : Type u} {V : Type v}
    (combine : V → V → V) (code : C → V)
    (inside : V → Prop) (good : C → Prop)
    (leq smaller : C → C → Prop)
    (hrefl : ∀ a, leq a a)
    (htrans : ∀ a b c, leq a b → leq b c → leq a c)
    (htotal : ∀ a b, leq a b ∨ leq b a)
    (hcompat : ∀ a b, leq a b → ¬ smaller b a)
    (closed : ∀ a b, inside a → inside b → inside (combine a b))
    (split : ∀ c, ¬ good c → ∃ a, ∃ b,
      smaller a c ∧ smaller b c ∧ code c = combine (code a) (code b))
    (table : List C)
    (complete : ∀ c, c ∈ table)
    (outside : ∃ c, ¬ inside (code c)) :
    ∃ c, good c ∧ ¬ inside (code c) := by sorry

end OPG500Counterexample

Source

Candidate C12, frozen finite-descent declaration: https://github.com/vibemathing/problem-opg-500-geodesic-cycles/blob/a41fe59b4535851ea55f6e868e938b9aaf81e924/research/artifacts/candidates/opg500-a01-c12/FiniteDescent.lean

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

Let $C$ and $V$ be types. Let combine : V\times V\to V, code : C\to V, inside : V\to\mathrm{Prop}, good : C\to\mathrm{Prop}, and let leq and smaller be binary relations on $C$ . Assume:

\begin{aligned} &\text{for every }a,\ \mathrm{leq}(a,a);\\ &\text{for all }a,b,c,\ \mathrm{leq}(a,b)\land\mathrm{leq}(b,c)\Rightarrow\mathrm{leq}(a,c);\\ &\text{for all }a,b,\ \mathrm{leq}(a,b)\lor\mathrm{leq}(b,a);\\ &\text{for all }a,b,\ \mathrm{leq}(a,b)\Rightarrow\neg\mathrm{smaller}(b,a);\\ &\text{if }a,b\text{ are inside, then }\mathrm{combine}(a,b)\text{ is inside};\\ &\text{for every }c\text{ that is not good, there exist }a,b\text{ with }\mathrm{smaller}(a,c),\ \mathrm{smaller}(b,c),\\ &\qquad\text{and }\mathrm{code}(c)=\mathrm{combine}(\mathrm{code}(a),\mathrm{code}(b)). \end{aligned}

Let table be a finite list of elements of $C$ containing every element of $C$ . If there exists some $c$ in $C$ for which $\mathrm{code}(c)$ is not inside, then there exists some $c$ in $C$ such that $c$ is good and $\mathrm{code}(c)$ is not inside.

Human review

Endorsed by Shuze Chen · Sep 7, 2026
Endorsed by hao jia · Sep 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph