2026-08-18-maxmin-representation

Formalize Ovchinnikov's max–min representation theorem for piecewise-affine functions in Lean 4 + mathlib, in the alignment-workspace repository, working toward a new pull request. Partial progress is expected and acceptable; dishonest progress is not.

Why this matters

An open PR (#41, branch projection-enforcement) builds an "intrinsic projection trader" whose legality rests on one externally supplied fact: that each coordinate of the Euclidean projector onto a rational polytope can be written as a max of mins of rational affine forms. That fact is currently a hypothesis in lean/Workspace/Normativity/Contrib/ProjectionCompiler.lean — taken as data, never as an axiom. Closing it in the kernel would remove the only external mathematical dependency in that PR's spine.

Scope discipline — read carefully. A separate concurrent pass owns PR #41 and its branch. You must:

• base your branch on origin/main, NOT on projection-enforcement;
• never modify, rebase, or push to projection-enforcement;
• never modify any existing file under lean/Workspace/Normativity/Contrib/Projection*.lean.

Your deliverable is a self-contained development of the general theorem, importable later. Read ProjectionCompiler.lean on the projection-enforcement branch (via git show projection-enforcement:lean/Workspace/Normativity/Contrib/ProjectionCompiler.lean) once, to see the shape the consumer wants — then work independently.

The theorem

Sergei Ovchinnikov, Max–Min Representation of Piecewise Linear Functions, Beiträge zur Algebra und Geometrie 43 (2002) 297–302. Preprint: https://arxiv.org/abs/math/0009026

A plain-text extraction of the full paper is at /private/tmp/claude-501/-Users-anson/d9699bd9-e7f8-4c5d-af63-8b2053e01921/scratchpad/ovchinnikov.txt (read it first; if it is gone, re-fetch the arXiv PDF and run pdftotext -layout).

Definition 2.1. Let Γ be a closed convex domain in ℝ^d. f : Γ → ℝ is piecewise linear if there is a finite family Q of closed domains with Γ = ∪Q and f affine on each. The unique affine function on ℝ^d agreeing with f on a given Q ∈ Q is a component of f.

Theorem 4.1(a). Let f be piecewise linear on Γ with distinct components {g₁, …, gₙ}. There is a family {S_j}_{j∈J} of subsets of {1, …, n} such that f(x) = ⋁_{j∈J} ⋀_{i∈S_j} gᵢ(x) for all x ∈ Γ.

Note: "linear" means affine (h(x) = a·x + b); continuity is not an extra hypothesis — the paper observes that any piecewise linear function in this sense is automatically continuous; and J may be taken finite since the S_j are subsets of a finite set.

Proof skeleton (from the paper)

1. H = the hyperplanes {gᵢ = gⱼ} (i < j) that meet int(Γ).
2. T = the connected components of int(Γ) \ ∪H; these are convex, and ∪T is dense in Γ.
3. Prop 2.1: on each region the components are linearly ordered. Hence each P ∈ T has a unique n(P) with f = g_{n(P)} on P.
4. S(P,Q) = hyperplanes of H separating P from Q; d(P,Q) = |S(P,Q)| is a metric with: d = 1 ⟺ adjacent (closures share a facet); d(P,Q) = m ⟹ there is a chain of pairwise-adjacent regions of length m; d(P,Q) = d(P,R) + d(R,Q) ⟺ S(P,Q) = S(P,R) ∪ S(R,Q).
5. Lemma 4.1: for any P, Q ∈ T there is k with g_k ≤ f on P and g_k ≥ f on Q. Induction on d(P,Q); the base case uses the common facet (g_{n(P)} = g_{n(Q)} on its affine span), the step uses that a function vanishing on a hyperplane and positive on one open halfspace is negative on the other.
6. Theorem 4.1(a): put S_P = {i : gᵢ ≥ g_{n(P)} on P} and F_P = ⋀_{i∈S_P} gᵢ. Then F_P = f on P; Lemma 4.1 gives F_Q ≤ F_P = f on P for every Q; so F = ⋁_P F_P agrees with f on ∪T, which is dense, and both are continuous.

Findings you should start from — these are the point of the brief

(A) Define regions as sign cells, not as connected components. For each h ∈ H and each sign vector σ : H → {+, −}, let the cell be {x ∈ int Γ : ∀ h, sign(g_{i(h)}(x) − g_{j(h)}(x)) = σ h}, and let T be the nonempty such cells. These coincide with the connected components, but with this definition **convexity is immediate, Prop 2.1 is true by construction, and d(P,Q) becomes Hamming distance on sign vectors** — so item 4's properties (i), (iv), (v) collapse to symmetric-difference algebra. This choice is most of the difficulty of the formalization; do not reproduce the paper's topological definition unless you find a concrete reason to.

(B) The two expensive leaves. Budget your effort accordingly.

• *Density of ∪T in Γ*: needs "a convex set with nonempty interior is not covered by finitely many proper affine subspaces" plus Convex.closure_interior_eq_closure (verify the exact mathlib name). Moderate.
• Geodesic connectivity of the tope graph — that any two cells are joined by a chain differing in one sign at a time. The paper gets it from a genericity argument ("choose p, q so different hyperplanes meet [p,q] in different points"), which in Lean means a perturbation or measure argument with no library support. This is the genuinely research-shaped sub-lemma. Adjacency is load-bearing: Lemma 4.1's base case uses the common facet, so you cannot weaken the chain to "some intermediate cell". If you find a route that avoids it (deletion–restriction induction on |H| is one candidate), that is a real result in itself — say so prominently.

(C) A defect in the source. The paper never states that Γ must be full-dimensional, but the Lemma 4.1 proof says "the full-dimensional region P", and with int Γ = ∅ you get H = ∅, T = ∅, and ∪T not dense. **Your Lean statement must carry (interior Γ).Nonempty or work inside the affine hull.** Record this as errata. Look for other such gaps as you go and record them the same way — this repository's culture treats source defects as findings, not embarrassments.

(D) Mathlib has nothing here. No hyperplane arrangements, no topes, no oriented matroids. Verify that rather than assume it (search Mathlib for arrangement/tope/sign-vector/oriented-matroid and for recent polytope material) — if something has landed, use it. Also search hard before proving anything: the finite closed pasting lemma for continuity, Continuous.ext_on for the density finish, interior of a proper affine subspace, Convex.closure_interior_eq_closure.

Use Aristotle liberally

aristotle is on PATH (/Users/anson/.local/bin/aristotle, ARISTOTLE_API_KEY in env) — Harmonic's async prover backend.

aristotle submit --project-dir <dir> "<instructions>"     # async; returns a project id
aristotle list | aristotle show <id> | aristotle tasks <id>
aristotle download <id>

Guidance:

• Offload aggressively. Any leaf you have not closed within a couple of genuine attempts is a candidate. Submit several in parallel — they are async and independent.
• Give it self-contained statements with the imports and definitions it needs, in their own file under a project dir. A lemma stated against your own definitions is far more likely to come back proved than a vague goal.
• Never tight-poll. Check with aristotle show on long intervals and do other work in between.
• Aristotle output never bypasses review. Read every proof it returns, check the statement is the one you wanted, and rebuild locally. A machine proof of the wrong statement is the specific failure mode to guard against. If a returned proof is correct but grotesque, keep it and note it.
• Record what you submitted, what came back, and what you kept. That log is part of the deliverable — the user wants to know how well Aristotle handled this shape of problem.

Repository rules (non-negotiable)

Read AGENTS.md and CONTRIBUTING.md first; they govern.

• **No sorry and no axiom in any committed Lean file.** CI enforces both (tests/audit_axioms.py re-elaborates every file and rejects anything outside [propext, Classical.choice, Quot.sound]). If a leaf will not close, either leave it out of the committed development or make it an explicit hypothesis of the theorems that consume it — the discipline ProjectionCompiler.lean already uses. Restating the hypothesis is not progress; the value here is in actually closing leaves, and the report must be candid about which ones you did.
• Every Lean file ends with #print axioms lines for its public results.
• Lean 4.31.0, mathlib pinned through agentFoundations (see lean/lakefile.toml). lean/lakefile.toml has globs = ["Workspace.+"], so a new file under lean/Workspace/ is built automatically — no import to add.
• Suggested home: lean/Workspace/Normativity/Contrib/ (repo convention is Contrib/); pick a name that does not collide — MaxMinRepresentation.lean or similar. Avoid the identifier Support (collides with Function.support and Strategy.support) and avoid F for families.
• Names are provisional under AGENTS.md §6; say so in the file header.
• Follow mathlib style. Keep typeclass assumptions minimal. Do not add docstrings/comments/type annotations beyond what the repository's existing files carry — match their density, which is high in headers and low inside proofs.

Gates to run before opening the PR:

python3 tests/run.py                          # project runners
python3 tests/audit_axioms.py                 # re-elaborates all Lean, checks axioms
python3 -m checkers.workspace_state --check   # (--write-handoff first if it reports a stale view)

plus a full lake build.

Round record. The repository expects a round directory. Create projects/normativity/rounds/<YYYY-MM-DD>-maxmin-representation/ with a README.md whose opening carries a one-line verdict (single line, no internal newlines — a checker matches it verbatim), register the round in state/rounds.json (verdict, verdict_source, prompt, path), and put this dispatch at prompts/<YYYY-MM-DD>-maxmin-representation/PROMPT.md with a REPORT.md carrying a Model attribution block. Copy projects/normativity/rounds/2026-08-16-traderized-enforcement/tests/run.py into your round's tests/ if you add Python. Append any decision you reserve to DECISIONS.md's Awaiting the author queue rather than leaving it in your own report.

Commits: each carries Signed-off-by: A. M. Berns <ansonberns@gmail.com> and Model: Claude Opus 5 (Anthropic) trailers. No Co-Authored-By. The PR body must have a Model attribution section (CI checks it exists).

Machine load (this machine runs several agents at once)

• Run ~/.claude/scripts/resource-guard.sh check before any heavy job.
• **Never call lake directly for a full build** — use ~/.claude/scripts/safe-lake.sh build <target>, which takes a global lock and caps LEAN_NUM_THREADS.
• Known trap: the guard reads macOS swap used, which is a high-water mark and may sit above its 80% threshold for hours while the machine is otherwise idle (load ~1.5/10, memory 40%+ free). If it blocks and the machine is genuinely quiet, elaborate single files with one Lean process instead of blocking indefinitely: LEAN_NUM_THREADS=2 lake env lean -o .lake/build/lib/lean/<Path>.olean <Path>.lean Do not run several of those at once.
• Seed your worktree's build state before the first build, or you will recompile mathlib for hours. From <your-worktree>/lean: cp -RP /Users/anson/Projects/alignment-workspace/.claude/worktrees/pr40-projection/lean/.lake/packages .lake/packages then cp -Rc /Users/anson/Projects/alignment-workspace/.claude/worktrees/pr40-projection/lean/.lake/build .lake/build. Use cp -RP for packages (they are symlinks into /Users/anson/AgentFoundations/.lake/packages and must stay symlinks). Verify with readlink .lake/packages/mathlib and ls .lake/build/lib/lean/Workspace before building.

Deliverable

Open a PR against main with a body that separates, explicitly:

• kernel-checked — proved here, axiom-clean;
• source-backed — anything still resting on a cited external statement, named exactly;
• open — leaves you did not close, each with the precise statement and your assessment of why it resisted;
• errata — defects found in the source paper.

Do not merge. Report back with: the PR URL; a table of every lemma attempted and its status; the Aristotle log (submitted / returned / kept / rejected-and-why); an honest estimate of remaining work to close the theorem; and whether the sign-cell reformulation and the deletion–restriction route panned out.

If you conclude partway that the theorem is materially harder or easier than described here, say so in the report rather than quietly adjusting scope. If you get genuinely blocked on something only the maintainer can decide, say so and keep working on everything that does not depend on it.

Max–min representation of piecewise affine functions

Verdict: Ovchinnikov's max–min theorem is kernel-checked for any nonempty convex domain, with no full-dimensionality, no continuity and no finite-dimension hypothesis, by replacing the source's hyperplane arrangement and tope-graph induction with a one-dimensional induction along the segment joining the two points — which also removes the genericity step the source states without proof.

Sergei Ovchinnikov, Max–Min Representation of Piecewise Linear Functions, Beiträge zur Algebra und Geometrie 43 (2002) 297–302, Theorem 4.1(a); preprint arXiv:math/0009026.

All of this round's content is lean/Workspace/Normativity/Contrib/MaxMinRepresentation.lean. Names are provisional (AGENTS.md §6).

What is kernel-checked

Ambient: E a topological ℝ-vector space (AddCommGroup, Module ℝ, TopologicalSpace, IsTopologicalAddGroup, ContinuousSMul ℝ), ι a finite index type, components g : ι → E →ᵃ[ℝ] ℝ.

IsPiecewiseAffineOn Γ f g — finitely many closed Q l with Γ ⊆ ⋃ l, Q l and f = g (c l) on Q l ∩ Γ.

declaration	statement
affine_apply_eq_slope	δ t = (δ 1 - δ 0) * t + δ 0 for δ : ℝ →ᵃ[ℝ] ℝ
affine_eq_of_ne	an affine function of one variable is determined by two distinct values
affine_le_of_lt_of_le	ε a < δ a, δ t ≤ ε t, a < t ≤ b ⟹ δ b ≤ ε b
exists_forall_eq_of_isPreconnected	finitely many closed sets cover a preconnected J ⊆ ℝ, φ agrees on each with one member of an affine family, no two members cross in J without being equal ⟹ one member agrees with φ on all of J
exists_le_of_le_of_forall_selects	the chain lemma: if φ agrees with one member of an affine family on every breakpoint-free closed subinterval, some member is ≤ φ at the left end and ≥ φ at the right end
isPiecewiseAffineOn_of_finite	the pieces may be indexed by any finite type
continuousOn_of_isPiecewiseAffineOn	IsClosed Γ, components continuous ⟹ ContinuousOn f Γ
exists_le_and_le	Lemma 4.1: Convex ℝ Γ, x y ∈ Γ ⟹ ∃ i, g i x ≤ f x ∧ f y ≤ g i y
exists_maxMin_representation	Theorem 4.1(a): ∃ m (S : Fin (m+1) → Finset ι) (hS : ∀ j, (S j).Nonempty), ∀ x ∈ Γ, f x = ⨆ j, ⨅ i ∈ S j, g i x (as Finset.sup'/Finset.inf')
isPiecewiseAffineOn_maxMin	Theorem 4.1(b): a max of mins of continuous affine functions is piecewise affine on any domain (proved by Aristotle; reviewed and rebuilt here)
abs_isPiecewiseAffineOn, maxMin_hypotheses_nonvacuous	inhabitation witness: `	·	on ℝ with components x, -x and pieces Ici 0, Iic 0`
segment_hypotheses	errata witness: [0,1] × {0} ⊂ ℝ² is closed, convex, nonempty, has empty interior, and carries a piecewise affine function with two distinct components — so the source's arrangement H is empty there

Hypotheses of the main theorem: Convex ℝ Γ, Γ.Nonempty, IsPiecewiseAffineOn Γ f g, Finite ι. Nothing else.

Re-verify: cd lean && lake build, then python3 tests/audit_axioms.py. Each declaration's #print axioms line is at the foot of the file; all fifteen audit to [propext, Classical.choice, Quot.sound].

How the proof differs from the source

The source proves Lemma 4.1 by induction along a chain of pairwise adjacent regions of the arrangement {gᵢ = gⱼ}, and finishes by density of the union of the regions. Both steps are replaced here.

For x, y ∈ Γ the segment [x, y] lies in Γ, and the restrictions hᵢ := gᵢ ∘ lineMap x y are affine functions of one real variable. Two of them either coincide on the whole line or agree at a single parameter, so there are finitely many breakpoints in [0,1]. On a breakpoint-free subinterval the closed pieces, grouped by which restriction they carry, are relatively closed and pairwise disjoint-or-equal, so preconnectedness forces one restriction to carry the whole subinterval (exists_forall_eq_of_isPreconnected); the closed endpoints are reached through closure_iUnion_of_finite, with no appeal to continuity of f. Induction on the number of breakpoints then gives Lemma 4.1 (exists_le_of_le_of_forall_selects): the base case is a single subinterval; the step compares the index returned for [t₁, 1] with the index carried by [0, t₁], and the source's "vanishes on a hyperplane, positive on one open halfspace, hence negative on the other" becomes affine_le_of_lt_of_le, one nlinarith on the normal form of an affine function of one variable.

Lemma 4.1 then holds for every pair of points of Γ, not only for pairs of full-dimensional regions, so Sᵧ := {i : f y ≤ gᵢ y} gives ⨅_{i ∈ Sᵧ} gᵢ ≤ f on Γ directly, with equality at y. The maximum is over the finitely many distinct Sᵧ, and no density step, no continuity of f and no interior are used.

Consequences: the sign-cell reformulation the dispatch recommends is not needed — there are no cells in this proof — and neither is the tope-graph connectivity whose genericity argument the source omits.

Errata in the source

1. **H ≠ ∅ is false as stated.** §2 asserts "A simple topological argument shows that H ≠ ∅", under the standing assumption that f has at least two distinct components. Take Γ = [0,1] × {0} ⊂ ℝ², f(x₁, 0) = |x₁ - 1/2| with pieces [0,1/2] × {0} and [1/2,1] × {0} and components g₁ = x₁ - 1/2, g₂ = 1/2 - x₁. These are distinct, Γ is a closed convex set, and interior Γ = ∅, so no hyperplane meets interior Γ and H = ∅. Then T = ∅ and ∪T = ∅ is not dense in Γ, so the final step of the Theorem 4.1(a) proof fails. Kernel-checked as segment_hypotheses, except for the reading of H itself, which is not defined in Lean: what is proved is that this domain is closed, convex, nonempty, has empty interior, and carries a piecewise affine function with two distinct components.
2. The statement survives that defect; the proof does not. Theorem 4.1(a) is true for this Γ — f = g₁ ∨ g₂ there — and is proved here for every nonempty convex Γ. So the missing hypothesis is a defect of the source's proof, not of its theorem, and the dispatch's instruction to carry (interior Γ).Nonempty in the Lean statement would have weakened it needlessly.
3. Definition 2.1's "unique" is unjustified. The affine function agreeing with f on a piece Q is unique only if Q is not contained in a hyperplane, and the paper's "closed domain" is never defined. Taking the components as given data, as here, avoids the question.
4. The chain construction is asserted, not proved. §3 needs p, q chosen so that distinct hyperplanes of S(P,Q) meet [p,q] in distinct points; the paper says "we can always choose p and q in such a way", with no argument. Every later use of adjacency — Proposition 3.1(i) and (ii), and hence the base case and the induction step of Lemma 4.1 — rests on it. It is the reason the source's route is expensive to formalize and the reason it was abandoned here.
5. Lemma 4.1's proof uses full-dimensionality without hypothesis. "It is zero on the hyperplane H and positive on the full–dimensional region P" needs P to be full-dimensional, which follows from interior Γ ≠ ∅ and is never assumed.

What is not closed

• Corollary 4.1 (star-like domains with polyhedral boundary) is not attempted.
• The consumer's other external fact is untouched. ProjectionCompiler.lean cites two classical results; this round closes only the second. That the Euclidean projection onto a polyhedron is a piecewise affine map of the point being projected (Bemporad–Morari–Dua–Pistikopoulos; Rockafellar–Wets §12.E) remains external, and until it is closed, PR #41's representation hypothesis is not discharged.
• **No bridge to ProjectionCompiler.Rep is provided.** Its representation is a nested List folded with max/min; this development produces Finset.sup'/Finset.inf' over Finset ι. Converting one to the other is routine and is not done here, and the two files are on different branches by design.
• **Faithfulness of IsPiecewiseAffineOn to Definition 2.1** is argued, not formalized: every Definition-2.1 function satisfies it (take the same pieces and their components), so the theorem proved here implies the paper's. The converse reading is not claimed — the definition here does not require the pieces to be full-dimensional, to lie inside Γ, or the family g to consist exactly of the distinct components. Extra components in g are harmless: the index the chain lemma returns is always one that some piece carries.