Hypostructure

Hypostructure is a Lean 4 framework for formalizing structural-exhaustion arguments: proofs organized as a finite tree of branch states, in which each step performs a case split, a local reduction, or a quantitative estimate, and either continues on a refined residual problem or closes its branch by contradiction. The framework provides a single typed representation of that structure, so that the bookkeeping such proofs depend on — which hypotheses are available on which branch, which obligations remain, which case splits are exhaustive — is checked by the elaborator rather than by inspection.

The repository contains the framework and its first application, a formalization of the minimal-counterexample proof of the Erdős–Gyárfás power-of-two cycle problem (Erdős problem 64). The manuscripts queued for subsequent formalization are in to_formalize/.

Design

The state of a branch is carried by one indexed type:

ExactLedger (Domain) (residual) (factKeys)

The active residual problem and the complete list of facts established on the branch appear as type indices. This placement determines the framework's properties.

Availability. A step declares its hypotheses in a FactManifest, and those keys are matched against the ledger's index at elaboration. Invoking a step on a branch that has not established its hypotheses is a type error, not an omission a referee must detect.

Retention. Commits prepend to the index. Every predecessor fact remains present and remains queryable at the refined residual, since each transition carries a RefinementSystem.Refines proof supplying the transport.

Absence of side channels. Each residual domain has one FactSystem, and FactSystem.value_subsingleton makes fact values proof-irrelevant. Data therefore cannot travel between steps inside a fact; anything a later step uses must be an observable of the object or a declared production of an earlier step.

Position independence. AtomicCT takes no predecessor parameter. A step runs after any branch cursor whose ledger contains its declared requirements, so a proof cannot encode an authored execution order and then rely on it.

Auditability. ExactLedger.audit reports the fact names and the chronological commits without exposing proof bundles; audit_complete certifies that the two views account for the same append-only history, audit_facts_unique excludes duplicate semantic facts, and audit_commits_nonempty excludes empty entries.

ExactLedger is the only carrier of residual state, proof history, and facts. The constraint is exclusive rather than preferential: no second carrier is permitted under any name, and a repository gate enforces this.

Components

Hypostructure/Core — the domain-neutral kernel

Problem.lean fixes the problem data: an ambient type, a baseline predicate, a branch state indexed by the ambient object, and optional typed presentation data. Target is separate, so one problem registration serves several theorem statements; its two bridge fields are formulation laws relating a target predicate to a public statement, and carry no mathematical content of the proof.

Residual/ExactLedger.lean defines the ledger described above. Its construction operations — root, append, publishFact, refine, initializeScope — require a FrameworkToken whose constructor is private and whose value is emitted by a custom elaborator only while compiling framework modules. Application modules cannot call them.

Strategy/ExactExecution.lean defines AtomicCT, the sealed executor. An executor receives a FactInputs view consisting of the current residual and exactly the facts named in manifest.Requires, and returns an AtomicResult committing exactly manifest.Produces. AtomicStrategy is a definitional alias of AtomicCT: there is no second executor, runner, conversion, or output type.

Execution.lean and Budget/ supply the executable substrate. A Spec fixes the input, outcome, and trace types of a computation; a Capability supplies a deterministic reference machine together with soundness, exhaustiveness, and a polynomial check budget agreeing with the machine's own count; the resulting Result has a private constructor, so a caller cannot present an unverified outcome as a verified one.

Routing.lean provides RoutedTask.selectFor and RoutedTask.dispatchFor, the only scheduling entry points. Both dispatch on exact keys in the branch index; declaration names are diagnostic.

Core also carries the finite mathematics the applications require: enumeration, partitions and connected partitions, maximal selection, certified table aggregation and bounds, finite entropy, dyadic length, and arithmetic transport.

Hypostructure/Graph — the finite-graph instantiation

Finite graph objects and their isomorphisms; boundaried atoms, gluing, and boundary overlap; deletion and deletion criticality; induced paths and maximal induced-path packing; window curvature algebra, enumeration, and codes; receiver load and routing; capacity-token accounting; and the Type A, Type B, cold-corridor, and route-8 machinery of the Erdős–Gyárfás argument.

These modules are stated in problem-agnostic terms. No framework module names the problem, and no constant of the manuscript — the window order 13, the label count 399, the surplus threshold, the barrier rate — occurs in the framework; each enters as a field of the registered presentation data. The order-generic curvature algebra remains in Graph/WindowCurvature, while everything fixed to a particular window order lives in the application.

Graph/Strategy/ holds the executable spine: SpineVocabulary (the Data record and the semantic keys with their Holds clauses), SpineRows (the rows, each an AtomicStrategy or a Decision), and SpineRun (the composition, its 21-exit Result, and the audit theorems).

Hypostructure/Fixtures — sealing tests

The fixture directory contains negative fixtures as well as positive ones: modules that are required to fail elaboration. A dropped fact, a duplicate fact, a missing requirement, and a breach of ledger opacity each have a fixture asserting rejection, so the sealing properties above are tested rather than asserted.

Gates

Three checks run under make lint. The total-execution gate rejects partial outcomes at the execution boundary. The canonical-ledger gate rejects declarations grafted into the canonical ledger's namespace and structures that impersonate it without instantiating FactSystem, and keeps quarantined legacy modules outside the build closure. The API-catalog check restricts the proof application to the generated plumbing allowlist in .agents/skills/eg-proof-expansion/references/allowed-api.md.

Repository layout

hypostructure/                   the framework (Lean 4, Mathlib)
  Hypostructure/Core/              domain-neutral kernel
  Hypostructure/Graph/             finite-graph instantiation and the spine
  Hypostructure/Fixtures/          positive and negative sealing fixtures
  Hypostructure/PDE/               pre-rewrite PDE instantiation (see Roadmap;
                                   outside the live build closure)
  scripts/                         the gates
proofs/hypostructure_erdos_64_eg/  the Erdős–Gyárfás application
to_formalize/                      manuscripts queued for formalization
EG_STRATEGYDAG_AUDIT.md            row-by-row port tracker
LEGACY_REMOVAL_AUDIT.md            record of what the API rewrite retired

Building

Requires elan. The toolchain is leanprover/lean4:v4.31.0, with Mathlib pinned to the corresponding tag.

make mathlib-cache     # fetch prebuilt Mathlib artifacts
make framework-build   # build the Hypostructure package
make erdos-build       # build the Erdős–Gyárfás application
make build             # both
make lint              # the three gates
make test              # build and lint

The Erdős–Gyárfás formalization

The statement is that every finite simple graph of minimum degree at least 3 contains a cycle whose length is a power of two. The public statement in proofs/hypostructure_erdos_64_eg/HypostructureErdos64EG/Problem.lean is pinned verbatim against Erdos64.erdos_64 of Google DeepMind's formal-conjectures.

The source is to_formalize/original_erdos_64_proof.tex, a minimal-counterexample proof that uses the Hegde–Sandeep–Shashank $P_{13}$-free theorem as a black box. Replacing the power-of-two-cycle predicate by the absence of edge-rooted Mersenne returns, minimality together with a boundaried replacement principle makes every proper atom target-uncompressible; the $P_{13}$-free theorem then forces a maximal packing of induced $P_{13}$ windows of low density, leaving a large $P_{13}$-free remainder. The curvature-rank branch routes rank loss to target defect, compression, or delocalization; the whole-graph case is handled by exact closed response profiles; the final closure is driven by two-budget entropy routing and a large-budget branch governed by a surplus-adjusted comparison.

The application boundary is two modules. Problem.lean declares the public statement, one Core problem, one Core target, and the single record of registered data the spine reads — the Hegde–Sandeep–Shashank theorem, via WindowAlgebra.lean, and an audited finite curvature table, via FiniteChecks/P13Barrier. It contains no strategy, no executor, and no ledger operation. StrategyDag.lean holds the authored topology.

Status

The proof is decomposed into 73 rows across eight blocks, tracked in EG_STRATEGYDAG_AUDIT.md. Each row records its paper statement, the statement read off the Lean type, the discrepancy between them, its ledger traffic, and its transport and terminals, followed by a table pairing every manuscript \label the row consumes with the declaration whose type states it. A blank implementation cell records that nothing in the tree implements the object.

Block	Rows	Status
A. Entry spine	1–10	Ported; compiles on the canonical ledger
B. Type A receiver ladder	11–19	Row 11 ported; 12–19 in rebuild
C. Type B fan	20–29	Rows 20–25, 29 ported; 26–28 open
D. Non-near-cubic surplus	30–36	Groundwork begun
E. Remainder, rank, net charge	37–42	Rows 37–38 ported; 39–42 in progress
F. Cold-window corridor	43–61	Rows 43–50 ported
G. Route-8 carrier closure	62–67	In rebuild
H. Rank-drop branch	68–73	In rebuild

The audit is subject to two standing conventions. A status cell is a claim about code as of the last review and is not itself evidence; only a build settles whether a row still holds. And docstrings, comments, node metadata, and earlier revisions of the audit are treated as unreliable: the admissible evidence for a row is the manuscript together with the Lean type, proof body, and registration site.

Every ported row has been checked with #print axioms and depends on propext, Classical.choice, and Quot.sound alone. There is no sorryAx, and no Lean.ofReduceBool, so no native_decide result is load-bearing.

The canonical-ledger rewrite

The framework was rewritten onto the single ExactLedger API, retiring a layered CT* stack of capability, certificate, search, and automation modules that AtomicCT.run replaces. This accounts for the blocks listed above as in rebuild: their mathematics is intact and quarantined on disk as porting reference, but a quarantined module is not re-imported, and each row is reconstructed against the live framework. LEGACY_REMOVAL_AUDIT.md records the removal and establishes that it does not change the build closure.

Roadmap

The manuscripts in to_formalize/ fall into three groups.

Methodology. branch_closure_methodology_extended.tex (Structural Exhaustion) is the reference manual: a typed library of proof tactics, a strategy manual for selecting and parameterizing them, and an assurance layer for auditing their inputs, outputs, and dependencies. Hypostructure/Core is an implementation of that specification. llm_auditable_proof_architecture_draft.tex develops the same method for PDE, replacing the search for a single decisive global estimate by iterated local closure, residual promotion, and certified reduction to previously discharged obstructions.

Combinatorics. original_erdos_64_proof.tex, in progress as described above.

Navier–Stokes. Four manuscripts forming a chain in which each discharges a hypothesis named by its predecessor.

• proof_setup.tex establishes the local pointwise Type I reduction: Seregin extraction, the raw generated state space, and exclusion of the small-amplitude, stationary $L^3$, uniformly $L^3$-tight, and structure-and-decay classes. Its Type I contradiction rests on one named residual-class hypothesis, p1:hyp:no-remainder, which the paper states explicitly.
• paperIV_residual_branch.tex proves that hypothesis. An ordered residual decomposition, centered angular-circulation absorption, a minimal mesoscopic-scale rigidity theorem, and an endpoint sequence-$L^3$ Liouville argument for bounded mild ancient solutions yield the refined residual closure; inserted into the setup paper's final assembly, this gives cor:local-typeI-unconditional, placing every finite-energy singular point in the local Type II alternative. No global critical-norm estimate and no global Liouville theorem for bounded centered profiles is used.
• type_II_regularity.tex establishes the local retained-branch exclusion criterion for the remaining alternative, by repaired-gauge representation for nondegenerate concentration cores, local Calderón–Zygmund pressure control, a Caccioppoli estimate on compact cylinders, multibubble and cascade reductions, and scale-collapse cost estimates, with the retained compact branch closed by routing into the scale-rigid discharge.
• ns_perelman.tex constructs a localized entropy functional $\mathcal{W}_{\mathrm{loc}}$ on the singular-branch state space supplied by the preceding three. It is conditional on those companions by construction, and serves as an organizing quantity for the program rather than as one of its exclusions.

overall_proof_architecture.tex is the referee guide to the stratification, and stokes_appendix_body.tex supplies supporting Stokes-system material.

Formalization order is governed by the framework rather than by the mathematics: a target is queued once its branch structure — its case splits, residual promotions, and retained obstructions — has been read off the manuscript and expressed as rows over the canonical ledger. The immediate items are:

1. Complete Erdős–Gyárfás: close the open rows, re-root StrategyDag.lean on Spine.run, and drive the argument to the pinned public statement. This is what demonstrates that the framework carries a complete proof end to end.
2. Formalize the assurance layer of branch_closure_methodology_extended.tex as theorems about ExactLedger.
3. Rebuild Hypostructure/PDE/. It predates the canonical-ledger rewrite and lies outside the live build closure; its parabolic atlases, localization, vorticity, and Navier–Stokes model are porting reference, to be reconstructed on the canonical API as the Erdős–Gyárfás rows are, rather than re-imported.
4. Port the Navier–Stokes chain in dependency order: proof_setup, paperIV_residual_branch, type_II_regularity, ns_perelman. The chain is itself an instance of the structure the ledger records. The setup paper names a residual-class hypothesis and promotes it; Paper IV discharges it and commits the corresponding fact; the final assembly reads that fact back. Under formalization the discharge becomes a key in the branch index, present or absent, and is checked at elaboration rather than traced by hand across manuscripts.

No schedule is claimed. What formalization adds is not qualification of the results but a mechanical record of their use: which branch each theorem closes, and which facts were available when it did.

Citing

Archived on Zenodo at 10.5281/zenodo.21813635. The concept DOI above resolves to the most recent release; each release also receives a version DOI.