Add roadmap: graph regularity, finite weak regularity, and arity-3 hypergraph complexes

[cameronfreer]

Status

Ready for roadmap review. The roadmap is self-contained against the pinned Mathlib: Suggested.lean imports only Mathlib, and no layer depends on any other in-flight roadmap — in particular, not on the dense graph limits roadmap (#53), which is an independent parallel analytic development (see Summary). (#53 and this PR both currently claim root-index position 14; whichever merges second needs a trivial index/import rebase.)

Summary

Adds a roadmap for a Tau Ceti library entry on the finite combinatorial regularity tower: graph regularity → finite weak (Frieze–Kannan) regularity → strong graph regularity → an arity-3 strong hypergraph regularity and induced-counting package. Mathlib already carries the finite-graph regularity ecosystem (SimpleGraph, edge densities, Finpartition/IsEquipartition/equitabilise, szemeredi_regularity, triangle counting/removal, SimpleGraph.Copy). The dense graph limits roadmap (graphons, the analytic cut norm, cut distance, analytic Frieze–Kannan, sampling) is an independent parallel analytic development: neither theory's theorems are derived from the other's, nothing here waits on it, and every finite–analytic comparison is an optional downstream adapter — never a layer dependency or an acceptance gate.

The local summit is deliberately stronger than a weak 3-uniform lemma: an arity-3 regular approximation of a hierarchy — vertex cells → ordered pair-color systems → pair cut-regularity → triads/polyads → relative top densities over polyads → top-type regularity — with an explicit approximant: the summit produces a colored 3-graph H' within a pinned edit discrepancy of the input H and regular over the complex's polyads, and induced counting is performed on H' — through an intrinsic placed-count formula — and transferred back to H through the edit bound. Top regularity is the counting-ready Rödl–Schacht/NRS test: subpolyads select arbitrary subgraphs of the parent polyad's three pair graphs, and regularity is tested against rank-r unions of them (vertex-box discrepancy is kept only as an honest weaker predicate). Top relations are colored/typed (not Boolean edge-only) precisely so induced counting controls both presence and absence. v1 stops at strong hypergraph regularity plus counting; induced removal, arithmetic applications, and exchangeable-array representations are named consumers, not the peak.

The roadmap follows the existing TauCetiRoadmap format:

• narrative README.md (conventions with inline rationale, consumed-Mathlib inventory, cross-roadmap dependency table, layer plan with per-layer prior-formalization notes, acceptance gates, an optional-interoperability paragraph, non-goals, references, reviewer checklist)
• Suggested.lean with compiled sorry-signatures
• root README.md index entry
• root TauCetiRoadmap.lean import

Suggested.lean pins 81 top-level declarations across Layers 0–9 that build green against the pinned Mathlib (lake build, verified locally; sorry is allowed in this human-owned roadmap library). It carries 33 sorrys: sixteen data targets whose exact formulas are later milestones — the bounds and schedules refiningRegularityBound / nestedRefinementBound / strongGraphRegularityBound / regularityBound3 / inducedCountingParameter3 / inducedCountingSchedule3 / inducedCountingRank3 / diagonalControl3, the counts and masses Colored3Graph.inducedCopyCount / placedInducedCopyCount / expectedInducedCountAt / expectedInducedCount / exceptionalPredictedMass3 / nontransversalPredictedMass3, and the constructors Subpolyad3.ofSubcells / TriadicComplex3.toHypergraphComplex — and seventeen theorem targets (energy monotonicity, the Layer-2 bridge, frieze_kannan, nested equitabilisation, strong regularity, the arity-3 summit, parameter and schedule positivity, the two charge-pinning inequalities, the rank lower bound, the placed counting theorem, the exceptional-route bounds on both the actual and predicted sides, the nontransversal actual-plus-predicted bound, the edit-transfer lemma, and the global counting theorem). Following the roadmap-writing guide, there are no def _ : Prop := sorry placeholders and no contentless Prop fields: predicate bodies that appear state real mathematical clauses in terms of the currently pinned data — in particular editDiscrepancy3 H H' is a real definition (unordered color disagreements between the input and the explicit approximant, at the ordered 6/|V|³ normalization), so Approximates3 has a fully concrete body, and expectedInducedCountAt's docstring pins the product shape of the prediction so it cannot be defined through inducedCopyCount.

It fixes the load-bearing choices so contributors don't oscillate:

• Graphs / partitions: finite graphs are SimpleGraph; partitions are Finpartition (univ) with P ≤ Q meaning P refines Q.
• Energy: the size-weighted weightedEnergy (the L²-of-block-average energy, monotone under refinement by Pythagoras), deliberately not Mathlib's unweighted Finpartition.energy (an offDiag average that is not Jensen-monotone under arbitrary refinement). Comparison with the dense graph limits roadmap's analytic graphonPartitionEnergy is optional interoperability, not a required adapter — the finite energy stands alone.
• Layer-2 bridge: exists_regular_equipartition_almost_refining carries an equipartition hypothesis on P₀, a large-V hypothesis, a complexity bound, and a real AlmostRefines containment clause — so the discrete partition is not a vacuous witness.
• Finite weak regularity is this roadmap's own (Layer 3): steppedCount, the count-scaled cutDiscrepancy (deliberately not called a "cut norm" — the analytic cut norm is the graphon roadmap's independent object), and a direct finite Frieze–Kannan theorem with the explicit 4^(⌈1/ε²⌉+1) bound; no graphon imports or analytic prerequisites.
• Strong graph regularity: StrongRegular carries a complexity bound in the starting complexity l₀ (not just uniformity + energy, which the discrete partition satisfies); the Layer 2 → Layer 4 connection is the named nested-equitabilisation bridge exists_regular_exact_refining_equipartition (Layer 2 outputs only an almost-refinement, StrongRegular iterates on exact nesting); and exists_strong_regular is compositional — starting equipartition P₀, requested minimum complexity l, almost-refinement conclusion.
• Colors: top relations are a total unordered Colored3Graph κ₃; pair colors use a separate palette on distinct ordered pairs ({p : V × V // p.1 ≠ p.2} → κ₂). Pair regularity is skeleton-relative (over actual cell pairs and their sub-cells).
• Hierarchy: Polyad3 S is built over a lower skeleton S and stores its three pair colors (not an arbitrary triple-support), with its three pair graphs and the Polyad3.ofData constructor exposed; Subpolyad3 is the Rödl–Schacht/NRS subtriad — arbitrary subgraphs of the parent's three pair graphs (vertex-subcell restriction only a constructor); top regularity is the color-indexed rank-r test IsTopRegularOverPolyad over unions of subpolyads, with the vertex-box form retained only as the honest weaker IsVertexBoxRegularOverPolyad, never consumed by the counting summit.
• Summit: TriadicComplex3 κ₃ chooses its own lower pair palette (Fin pairColorCount), so exists_strong_regular_approximation3 does not assume an arbitrary fixed κ₂ works — and it quantifies an explicit approximant H', tied to H by the real editDiscrepancy3, so the discrepancy compares two colorings that both exist. IsStrongRegularApproximation3 H H' C ε F r t₀ bundles approximation-to-H, a real IsPolyadDecomposition (disjoint + covering, so exceptionalPolyadMass is not vacuous), lower-skeleton regularity, (F C.complexity, r)-top-regularity of H' over most polyads (exceptional-mass bound ε), and a complexity bound (via regularityBound3 depending on the top palette size, the rank, and the vertex floor t₀ — the floor must feed the bound, else the summit is false for t₀ above a t₀-independent bound) — where C.complexity is computed from the structure (vertex cells + pair colors + polyads), never a free stored field, so the bound genuinely controls the complex. The summit's conclusion additionally carries VertexCellsControlled C t₀ — equitable vertex cells with a requested complexity floor — the diagonal-gate input the counting layer consumes.
• Counting: expectedInducedCount H' C F₀ is intrinsically specified — a sum over placements (PatternPlacement3, PairColorPlacement3) of a pinned product of cell-size, pair-color-density, and top-color-relative-density factors, never defined through inducedCopyCount (which would hide the counting theorem inside the definition) — with pair colors assigned to one canonical orientation per pattern pair (i < j), never both marginals, whose joint correlation pair regularity does not control. The real counting lemma is the placed local theorem placed_induced_counting3 — at transversal placements with top-regular routes (IsTopRegularRoute: every polyad the route induces is one the approximation actually controls — the strong approximation guarantees top regularity only over most polyads, so an unrestricted route could pass through an exceptional polyad where hreg supplies nothing), counting in the approximant H' (per-placement counting in H would be false: a small global edit discrepancy can concentrate inside one placement), at the per-route budget of the ε/6 placed charge — routeBudget3 C k (ε/6) with routeBudget3 = ε / max 1 (q₂^(k choose 2)): a placement admits up to q₂^(k choose 2) routes, and allocating the full ε to placed counting would exhaust the budget before the remaining steps. The regularity runs at a genuine schedule inducedCountingSchedule3 : ℕ → ℝ (local strengths — LowerSkeletonRegular evaluates it at the lower complexity #cells + #pair-colors, TopRegularOverMostPolyads at C.complexity; positive everywhere by inducedCountingSchedule3_pos, as the summit's hF requires), deliberately separate from the global edit/exceptional parameter inducedCountingParameter3. The global induced_counting_from_strong_regular_complex3 splits the final ε into six explicit ε/6 charges across four steps, each closed by a pinned target: (1) the budgeted placed theorem on transversal, top-regular routes; (2) the discarded routes bounded on both sides — actual mass by exceptional_route_mass_le (at most k³·exceptionalPolyadMass·|V|^k tuples) and predicted mass by exceptionalPredictedMass3 / exceptional_route_prediction_mass_le (separate εmass/εcount so the lemma is instantiable without an unpinned comparison; the schedule charged at the lower complexity it is actually supplied at; the route-count factor q₂^(k choose 2) in the slack), their fits pinned by the charge inequalities inducedCountingParameter3_charge (k³·parameter ≤ ε/6) and inducedCountingSchedule3_charge (k³·ℓ^(k choose 2)·schedule(ℓ) ≤ ε/6); (3) the diagonal floor VertexCellsControlled C (diagonalControl3 F₀.k ε) bounding the omitted nontransversal placements — actual and predicted, pinned by nontransversal_actual_and_predicted_mass_le — at its ε/6 charge; (4) the named, inherently global edit transfer inducedCopyCount_edit_transfer from H' to H (fit again by the parameter charge) — predicting the induced count in the original H at the pattern-size error scale |V|^{F₀.k}, with the rank pinned ≥ 1 (one_le_inducedCountingRank3 — rank 0 is vacuous on nonempty polyads).

Prior formalization

Much of the roadmap is already proved in the public Lean 4 library cameronfreer/regularity-lemmata — sorry-free, no custom axioms (CI-enforced), whose partition/graph layers are developed for directed relations on an arbitrary Finset host (its hypergraph development is Boolean and unordered); declaration-level claims are pinned at commit f7403c9. Proved there: the mass-weighted energy layer; the two-partition almost-refining bridge (the self-regular form remains this roadmap's open Layer-2 target); the finite Frieze–Kannan theorem, of which Layer 3's targets are the SimpleGraph specialization; a strong-witness theorem plus a closely related binary-palette counting analogue (Layer 4's gate itself stays open); Boolean precursors of the arity-3 summits — including the edited summit whose deletion-only subgraph is the Boolean specialization precedent for Layer 8's explicit-approximant architecture, and the disc/polyad test surfaces (IsDiscRegularAt, IsPolyadRegularAt … r) that Layer 7's rank-r top regularity aligns with by design; and the transversal/diagonal-gate counting architecture behind Layer 9. The roadmap's per-layer Prior formalization notes record the exact shape deviations a TauCeti implementation must reconcile. The analytic parallel is cameronfreer/graphon.

Roadmap shape

The roadmap organizes the development into ten layers (0–9):

0. finite colored graph and 3-uniform vocabulary — UniformHypergraph/edgeDensity, the total unordered top-coloring carrier Colored3Graph κ₃, colored/hypergraph copy-counts and densities (with the card V < r ⇒ density 0 convention)
1. partitions, block densities, refinement, energy — the size-weighted weightedEnergy and its refinement-monotonicity (Mathlib's increment boost machinery is a proof template — it is stated for the unweighted energy — not a direct consume)
2. Szemerédi graph regularity bridge — a regular equipartition almost-refining a given equipartition with a complexity bound (bridging to szemeredi_regularity, not duplicating its SimpleGraph statement)
3. finite weak regularity — steppedCount, the count-scaled cutDiscrepancy with its eliminator cutDiscrepancy_le_iff, and the direct finite Frieze–Kannan theorem frieze_kannan (bound 4^(⌈1/ε²⌉+1)), with frieze_kannan_cutDiscrepancy derived from it — self-contained, no graphon imports or analytic prerequisites
4. strong graph regularity — the named Layer 2 → 4 nested-equitabilisation bridge exists_regular_exact_refining_equipartition, StrongRegular (coarse/fine equipartitions, uniformity, weighted-energy gap, complexity bound in the starting complexity l₀), and the compositional exists_strong_regular (starting equipartition, minimum complexity, almost-refinement conclusion) plus a counting lemma consuming it
5. hypergraph complexes; vertex cells and pair-color systems — HypergraphComplex (consumed via the Layer-8 bridge), PairColorSystem (distinct ordered pairs), PairSkeleton3, the skeleton-relative IsPairColorRegular, LowerSkeletonRegular
6. triads, polyads, subpolyads, relative densities — Polyad3 S over a lower skeleton (cells + three pair colors, with Polyad3.ofData and the three pair graphs pairSupport₀₁/₀₂/₁₂), Subpolyad3 in the NRS subtriad form (arbitrary subgraphs of the parent pair graphs; ofSubcells a constructor), color-indexed relDensityOn / relativeDensity
7. top-layer regularity over polyads — the rank-r IsTopRegularOverPolyad (per color, over unionSupport of at most r subpolyads; r = 1 is the disc form), with IsVertexBoxRegularOverPolyad the honest weaker predicate
8. strong arity-3 regular approximation (summit) — TriadicComplex3 κ₃ (chooses its pairColorCount; complexity computed from the structure; toHypergraphComplex bridge), the explicit approximant H' with the real editDiscrepancy3 and Approximates3, IsPolyadDecomposition, exceptionalPolyadMass/TopRegularOverMostPolyads (for H', at rank r), VertexCellsControlled, IsStrongRegularApproximation3 H H' C ε F r t₀ with regularityBound3 q₃ ε F r t₀ (the vertex floor feeds the complexity bound — a t₀-independent bound would make the summit false for large t₀), exists_strong_regular_approximation3 (for every rank r and vertex floor t₀, under regularityBound3 … ≤ |V|; existential over both H' and the complex)
9. induced counting and embedding — FiniteColored3Pattern, inducedCopyCount, the placement layer PatternPlacement3 (+ Transversal) / PairColorPlacement3 (one pair color per canonically oriented pattern pair i < j — never both marginals) with its route-level control PairColorPlacement3.polyad / IsTopRegularRoute, placedInducedCopyCount and the pinned expectedInducedCountAt / expectedInducedCount H' C F₀, the global parameter inducedCountingParameter3 and the genuine schedule inducedCountingSchedule3 : ℕ → ℝ (+ positivity, needed for the summit's hF; deliberately separate roles), the charge-pinning inequalities inducedCountingParameter3_charge / inducedCountingSchedule3_charge (every global charge fits its ε/6 fraction, the schedule charge carrying the route-count factor ℓ^(k choose 2)), inducedCountingRank3 (pinned ≥ 1) / diagonalControl3 with its charge pinned as a theorem (nontransversalPredictedMass3 / nontransversal_actual_and_predicted_mass_le: the sum of both sides omitted by transversal counting — actual repeated-cell tuples plus predicted nontransversal mass — at most ε/6·|V|^k under the floor), the per-route budget routeBudget3 (ε / max 1 (q₂^(k choose 2)) — bare per-route errors cannot sum over the route count to the global bound), the placed local theorem placed_induced_counting3 (the real counting lemma: transversal placements with top-regular routes, counting in the approximant H', at the per-route budget of the ε/6 placed charge), the discarded-route bounds on both sides (exceptional_route_mass_le for actual mass; exceptionalPredictedMass3 / exceptional_route_prediction_mass_le for predicted mass — with separate εmass/εcount, the schedule charged at the lower complexity it is supplied at, and the route-count factor in the slack), the named global edit transfer inducedCopyCount_edit_transfer, and the global induced_counting_from_strong_regular_complex3 (the final ε split into six explicit ε/6 charges across four steps: budgeted placed counting on transversal top-regular routes + discarded-route bounds (actual, predicted mass, predicted route-slack) + diagonal gate + edit transfer)

It also records the eight pinned design conventions (with inline rationale), the entry-point-checked consumed-Mathlib inventory, the cross-roadmap dependency table (Mathlib / dense graph limits as independent parallel theory / exchangeability), per-layer prior-formalization notes with a summary section, the acceptance gates, the optional-interoperability paragraph, a non-goals section, and a reviewer checklist.

Files changed

README.md                                     (root index entry)
TauCetiRoadmap.lean                           (root import)
TauCetiRoadmap/Regularity/README.md
TauCetiRoadmap/Regularity/Suggested.lean

Verification

• lake build green at Lean v4.31.0-rc1 / Mathlib 9caeba1000ef8f302920981f4a08651d325abc81 (33 sorry warnings only — the data-def / theorem targets listed above).
• Suggested.lean imports only Mathlib because the finite roadmap is self-contained: Layer 3 is finite weak regularity with no graphon prerequisites, and analytic comparison adapters are out of scope (the README's Optional interoperability paragraph).
• Consumed Mathlib entry points and the quoted szemeredi_regularity signature checked directly against the pin; every regularity-lemmata declaration cited in the README verified to resolve in that repository; no existing Mathlib hypergraph carrier was found to reuse.

Authorship

Authored by Cameron Freer, with the assistance of GPT Pro 5.5, Claude Code (Opus 4.8 and Fable 5), Codex (GPT 5.5 and 5.6 Sol), lean4-skills, and lean-lsp-mcp.