Ordinal certificates and exact pruning characterize sequence realization
Alexander (2013), Section 6, asks whether the infinite gendered populations realizing a possibly avoidable sequence can be characterized, particularly using ordinal numbers. For a target s, use reachable vertex/phase states (v,k), witnessed by a path spelling the first k letters, with successors consuming s(k). Can avoidance be characterized by a decreasing ordinal certificate, and can finite-branching realization be characterized exactly by iterative removal of states without continuing children? This addresses ordinal membership and exact matching continuation, not a requirement that different avoiders receive different transfinite ranks.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Infinite labelled graphs; ordinal ranks
- Posed by
- Samuel A. Alexander, Biologically Unavoidable Sequences (2013), Section 6, published p.12; exact ordinal-membership and reachable-state interpretation.
- Year posed
- 2013
- Years open
- 13y
- Solved
- 2026-09-29
- Model
- OpenAI Codex (GPT-6 family)
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 8 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Avoidance is equivalent to a strictly decreasing ordinal certificate on the reachable states; arbitrary vertex/label types are allowed. Under finite per-label branching, natural certificates suffice. It also proves that states surviving every finite pruning round form the greatest successor fixed point and are exactly those with infinite continuations. A start realizes the full target iff its phase-zero state survives. Every other state has an attained finite maximum h, is removed at round h+1, and has a pointwise least natural certificate, even in populations realizing the target elsewhere. Complete finite-fibre blow-ups preserve corresponding least heights. Reachability prevents confusing an unrelated suffix with the original word. These are classical well-founded and finite-branching methods made exact in the source setting. This is not a deciding algorithm for arbitrary infinite inputs or a rank hierarchy separating avoiders; the artificial-root history tree is a different object.
What the AI did
A human collaborator selected the research directions and requested source correspondence, explanations, proof checking and submission. Codex agents developed the concrete mathematical construction or deduction, Lean proofs and exposition. Other agents in the project reviewed the arguments and source correspondence. These are internal project checks, not independent human expert review. Model-led discovery of the submitted scoped result is claimed; independent human verification and worldwide priority are not claimed.
Verification
Checked here on 30 September 2026 to the extent the artefacts allow. Lean 4.33.1 with Mathlib pinned at 0df444a3; the manifest records four new modules with 42 selected endpoints and three reused with 21, permitting only propext, Classical.choice and Quot.sound, and the Verify workflow is green on the correct repository. Not rebuilt here and no independent audit of the informal-to-formal correspondence, so Lean-checked. The source URL was corrected for the repository's trailing dash. Partial, as submitted: the ordinal-certificate and pruning characterisations answer a precise reading of Alexander's question and the submitter is explicit that they do not deliver every richer classification the section may have intended.
Sources
- Lean proofPinned public research note, Lean source and verification receiptsGeneric ordinal-certificate equivalenceExact surviving core and actual realizationLeast attained finite ranks in the complementExact height transport through complete blow-up
- Problem recordOriginal ordinal-characterization question, section 6
- OtherNew statement/definition scope reviewFrozen proof and log manifestSuccessful integrated hosted proof audit
Submitted by ZestyDingo473 on