feat(language): a model writes its formulations out on request, and states what each assumes of its data

[FBumann]

Prompt: "Lets work on a PR stacked onto that. It should achieve: 1. establish Spec->Spec transformations that expand sos and piecewise, making the transformations observable (they are currently done in lpspec depending on the used solver) 2. Put all the data assumptions of piecewise into the assumptions block. Look at #579 for the details" — "Take care, 582 might be based on a different piecewise implementation. Take care of checking that the new PR is written against #592" — "I want a clear table that shows which kind of piecewise holds which assumptions, and how they are spelled in the yaml" — "The table should hold the actual yaml syntax!" — "Can you add the typesetting to the table?" — "Transpose the table!" — "Make convex read the link sign and update the PR"

Prompt: "Review the stack of 602 and below" — "Yes: delete bound: and require bounds.upper on a set's member — fix the typesetting — fix the expand cache"

Note

The following content was generated by AI.

Closes #579. Replaces #582, which is this work on a base that predates #566, #585 and #589. Spec.expand() writes a formulation out on request, sos: is the second formulation, and what a piecewise: method assumes of its numbers is an ordinary predicate rather than a closed union only this package can read.

Stacked on #592. The chain is 566 → 589 → 592 → this, and every rung carries main at 0.0.0-alpha.110.

What a method assumes of the data

A cheap method is exact only for numbers of the right shape. Which conditions a block states is the method:'s business, and expand() writes each one into assumptions: verbatim as below. Each column is one condition, read top to bottom.

Read with: breakpoints x (the input axis) and y (the output), over dimension bp. on_curve is the dtype: bool parameter points: names, marking which breakpoints the curve actually runs through.

	<block>_increasing	<block>_curvature, convex	<block>_curvature, concave	<block>_curvature, either way	<block>_breakpoints	<block>_contiguous
Assumes	breakpoints strictly increase	the curve is convex	the curve is concave	the curve bends one way only	at least two breakpoints	the mask marks one run
Stated by	convex, lp	convex or lp, link bounded >=	convex or lp, link bounded <=	convex, both links pinned	lp	any method with points:
holds:	shift(x, along=bp, offset=1, edge=0) < x	(y - shift(y, along=bp, offset=1, edge=0)) * (shift(x, along=bp, offset=-1, edge=0) - x) <= (shift(y, along=bp, offset=-1, edge=0) - y) * (x - shift(x, along=bp, offset=1, edge=0))	the same, with >=	count(⟨bends up⟩ AND ⟨interior⟩, over=bp) == 0 OR count(⟨bends down⟩ AND ⟨interior⟩, over=bp) == 0, where a bend is the cross-product to the left and ⟨interior⟩ is the where: below it	count(x, over=bp) >= 2	count(on_curve AND NOT shift(on_curve, along=bp, offset=1), over=bp) == 1
where:	position(bp) > 0	position(bp) > 0 AND position(bp) != -1	the same	— (folded into the counts)	—	—
As typeset	$\mathrm{x}_{p \boxminus_{0} 1} &lt; \mathrm{x}_{p} \quad \forall, p \in \mathcal{P} ,:, \mathrm{pos}(p) &gt; 0$	$\left( \mathrm{y}_{p} - \mathrm{y}_{p \boxminus_{0} 1} \right) \cdot \left( \mathrm{x}_{p \boxplus_{0} 1} - \mathrm{x}_{p} \right) \le \left( \mathrm{y}_{p \boxplus_{0} 1} - \mathrm{y}_{p} \right) \cdot \left( \mathrm{x}_{p} - \mathrm{x}_{p \boxminus_{0} 1} \right) \quad \forall, p \in \mathcal{P} ,:, \mathrm{pos}(p) &gt; 0 \wedge \mathrm{pos}(p) \neq \lvert \mathcal{P} \rvert - 1$	the same, with $\ge$	$\lvert \{ p : \langle\text{up}\rangle \wedge \langle\text{int}\rangle \} \rvert = 0 \ \vee\ \lvert \{ p : \langle\text{down}\rangle \wedge \langle\text{int}\rangle \} \rvert = 0$	$\lvert \{ p \in \mathcal{P} ,:, \mathrm{x}_{p} \text{ is defined} \} \rvert \ge 2$	$\lvert \{ p \in \mathcal{P} ,:, \mathrm{on\_curve}_{p} \wedge \neg, \mathrm{on\_curve}_{p - 1} \} \rvert = 1$

\boxminus_{0} is the translation with a zero fill — one breakpoint back, the vacated row excluded by the where:.

adjacency and sos2 state nothing. They spend binaries and take a curve of any shape, so neither has a column above.

Under a points: mask every position test is replaced by the mask. Each where: narrows to the admitted neighbours — on_curve AND shift(on_curve, along=bp, offset=1) for a segment, the same with offset=-1 added for a bend — the breakpoint count reads count(on_curve, over=bp) >= 2, and the either-way column carries on_curve inside its counts rather than position(bp). This is what makes a ragged curve safe: without a mask the frame is rectangular, so a curve using three of five breakpoints has two rows whose missing data reads as a breakpoint at the origin.

The bounded link's sign fixes the direction of the bend, under both methods. lp states one side of the curve as its segment lines and convex relaxes the weights onto the hull, whose boundary on that side is the same set of points. So a >= link asks for a convex curve and a <= link for a concave one, whichever of the two methods is written.

Only a block with two pinned links states the weaker condition. There nothing in the block says which way the weights are driven within the hull, and "one bend either way" is the most that can be claimed: it rules out a mixed curve, which is wrong whichever way the pressure runs, and admits a single bend, which is exact one of the two ways. That is why that column is a disjunction of two counts rather than one comparison.

Each entry also carries a description:, the sentence a consumer raises when the data fails it. For the convex column:

piecewise 'curve': method: lp is exact only for a convex curve, and 'y' over 'x' along 'bp' is not one, so the answer is wrong rather than loose. Use method: adjacency or sos2, which take a curve of any shape.

A model that still declares the block derives the same text at load, so to_program(spec).assumptions == to_program(spec.expand()).assumptions.

The two long cells in full

The either-way holds:, which is what a method: convex block with both links pinned states:

holds: count((y - shift(y, along=bp, offset=1, edge=0)) * (shift(x, along=bp, offset=-1, edge=0) - x) > (shift(y, along=bp, offset=-1, edge=0) - y) * (x - shift(x, along=bp, offset=1, edge=0)) AND position(bp) > 0 AND position(bp) != -1, over=bp) == 0 OR count((y - shift(y, along=bp, offset=1, edge=0)) * (shift(x, along=bp, offset=-1, edge=0) - x) < (shift(y, along=bp, offset=-1, edge=0) - y) * (x - shift(x, along=bp, offset=1, edge=0)) AND position(bp) > 0 AND position(bp) != -1, over=bp) == 0

and its typeset form:

$$\lvert \{ p \in \mathcal{P} : \left( \mathrm{y}_{p} - \mathrm{y}_{p \boxminus_{0} 1} \right) \cdot \left( \mathrm{x}_{p \boxplus_{0} 1} - \mathrm{x}_{p} \right) > \left( \mathrm{y}_{p \boxplus_{0} 1} - \mathrm{y}_{p} \right) \cdot \left( \mathrm{x}_{p} - \mathrm{x}_{p \boxminus_{0} 1} \right) \wedge \mathrm{pos}(p) > 0 \wedge \mathrm{pos}(p) \neq \lvert \mathcal{P} \rvert - 1 \} \rvert = 0$$

$$\vee\ \lvert \{ p \in \mathcal{P} : \left( \mathrm{y}_{p} - \mathrm{y}_{p \boxminus_{0} 1} \right) \cdot \left( \mathrm{x}_{p \boxplus_{0} 1} - \mathrm{x}_{p} \right) < \left( \mathrm{y}_{p \boxplus_{0} 1} - \mathrm{y}_{p} \right) \cdot \left( \mathrm{x}_{p} - \mathrm{x}_{p \boxminus_{0} 1} \right) \wedge \mathrm{pos}(p) > 0 \wedge \mathrm{pos}(p) \neq \lvert \mathcal{P} \rvert - 1 \} \rvert = 0$$

The concave holds:, which is the convex one with the relation flipped:

holds: (y - shift(y, along=bp, offset=1, edge=0)) * (shift(x, along=bp, offset=-1, edge=0) - x) >= (shift(y, along=bp, offset=-1, edge=0) - y) * (x - shift(x, along=bp, offset=1, edge=0))
where: position(bp) > 0 AND position(bp) != -1

What else this changes

spec.expand(*kinds) — 'piecewise', 'sos', or nothing for both, in that order whatever order they are asked in. It returns a plain Spec; _ExpandedSpec is deleted, and resolved plus the record of what a curve derived live on Spec itself. to_yaml() refuses on an expansion that derived parameters, and names typeset as the reader's route. A full expand() reuses the curve expansion the load already cached rather than building and validating it again.

sos: is a formulation — it states <set>_seg, <set>_pick (<= 1), and two linking rows that hold an unpicked member at zero from both sides. Every coefficient is read off the member's own bounds:, so a negative bound and one the data carries are both admitted, and a set's member has to declare bounds.upper. The set carries no coefficient of its own: big_m: is gone, because a number below the member's bound capped a picked member the set does not cap, one above it was a looser row than the bound already states, and a solver taking the set natively ignored it either way — one file meant two models, which is the divergence fluxopt/specsolve#1702 records. method: adjacency is method: sos2 written out.

The typesetter prints what it was handed — a piecewise: block is one line, and typeset no longer expands. The three typeset verbs take --expand, because a shell cannot compose spec.expand(). typeset_declaration finds a derived assumption by name on the unexpanded model too.

Increasing, Curved, AtLeastTwo, Contiguous and Check are gone, and Assumption is Holds.

A how-to shows the two readings. docs/howto/see-an-expansion.md runs one model that states a curve and a set, and puts the construct beside the rows it stands for.

Why

An expansion that happens behind the author is a model they cannot read. Stating it on request makes the two readings one call apart — for review, for teaching, and for the engine that has no concept of a set, which can now refuse the model and name the rewrite instead of performing it (fluxopt/specsolve#1702).

The conditions follow the same thought. A rewrite that is exact only under a condition should say that condition in the language, beside the rows it writes — so a consumer reads one mapping with one kind in it, and a written-out model is not the way a model loses its data contract.

Why a bounded method: convex block was under-checked before this

_curvature_required answered 'either' for every convex block, whatever its links said, and read the sign only under lp. That is not the condition the formulation rests on.

method: convex lets the weights range over the hull the breakpoints span. A bounded link binds from one side of it: under y >= sum(lam * y_bp) the solver drives sum(lam * y_bp) onto the lower boundary of the hull, which is the curve itself only where the curve is convex. So a concave curve under method: convex with a >= link passed every condition the block stated, and the solve read the chord between the first and last breakpoint instead of the curve — wrong, not loose. method: lp states that same boundary as its segment lines and has read the sign since it existed; the two are one relaxation in two spellings.

The answer for a block with two pinned links is unchanged. It is also the only column this PR could have shortened and did not: the disjunction of two counts is what "one bend, either way" needs, and it is now stated only where the direction genuinely cannot be read off the file.

mutation	result
convex returns 'either' without reading the sign (the answer before this commit)	caught — the two new _CURVATURE_CASES rows fail
the pinned arm deleted, so a pinned block reads a sign it has not got	caught — convex-pinned-both-ways-states-a-single-bend, both test_a_curve_prints_what_its_method_assumes_of_the_breakpoints cases, and all three golden files fail

Why this replaces #582 rather than continuing it

#582 forked at main before #566, #585 and #589. Merging the chain into it conflicts in 18 of the 42 files it touches, and three things it is written against no longer exist:

• PiecewiseDeclaration.checks and check_message. A curve's conditions stand in Program.assumptions since feat(language): a model declares what it assumes of its data #589. reading.md's paragraph on checks is the assumptions section, and the invariant test reads that mapping.
• program.Walk is Direction, and ParameterDefinedNode is ParameterDefined — both refactor(program): a program names its nodes by the naming rule and its groups as the file does #585's renames.
• assumptions_of read the expansion record, so a curve's conditions vanished from the document the moment typeset stopped expanding. It reads the block instead.

The four commits are re-applied here rather than replayed, and #582 stays open until you close it. The hard rule is never to force-push.

The break

• big_m: is removed, with no key in its place. The closed schema's own error names the valid keys.
• A sos: block is refused at load unless each side of its member carries a coefficient: bounds.lower, and bounds.upper or domain: binary. A model whose member is unbounded on a side stops loading.
• A piecewise: block prints as a curve rather than as its expansion. Every consumer of the typeset output sees different math for the same file.
• A file that names a declaration an expansion emits is refused at load, and that now includes the four assumption names a block states.
• Program.sos loses big_m, and Resolved carries piecewise and assumptions.
• Increasing, Curved, AtLeastTwo, Contiguous and Check are removed from math_spec.program. A consumer matching on them matches Holds instead, and reads description for the sentence it used to get from check_message. The derived names lose their space: cost_curve increasing is cost_curve_increasing, which is a name the collision check now reserves.
• A method: convex block with a bounded link states convex or concave where it stated either. A curve that bends the wrong way for its link now fails the block's own condition when the data binds.

Why the curvature test is a cross-product, and what the neighbour terms need

The bend at a breakpoint compares the slope behind it with the slope ahead. Written as two quotients it would divide by a run that only the increasing condition rules out, so it is written as a cross-product instead.

A block with two pinned links has to count rather than compare. Which way the weights are driven within the hull is a fact about the rest of the model, so the claim is about the whole axis — one bend in either direction — rather than about a breakpoint. This is what #592's count() and shift() over a predicate were needed for, and it is why this PR sits on that one.

A translation over a variable-free expression needs an explicit edge=; the language refuses it otherwise and says a where: alone does not lift it, because the check is on the expression. So each neighbour term is edge=0 under a where that excludes the vacated row — the third spelling that refusal names.

Gates

pixi is not installed in this environment, so the gates ran from a uv environment on Python 3.12 with the pinned ruff==0.16.1 and pyrefly==1.2.0. That is a departure from the "prefix every command with pixi run" default.

On the head commit:

gate	result
pytest -q -n 4	1538 passed, 1 skipped (#592's head: 1467 passed, 1 skipped)
ruff check, ruff format --check	clean, 141 files
pyrefly check	0 errors, 10 suppressed
python -m tools.schema, python -m tests.typesetting.golden, the notation and gallery generators	regenerated; the schema loses the bound property and nothing else moves
render-tex	31 models rendered
mkdocs build --strict	clean, with the docs.python.org inventory dropped for the run, which the proxy refuses with 403
prettier --check	clean at 3.8.1 on the two pages the earlier commits changed, which is not the pinned version; not run for the review commit
compile-tex, typos, reuse lint	not run — the tools are not installed here. CI runs all three

Every rung of the stack was gated on its own after the review round: 1398 passed at #566, 1426 at #589, 1467 at #592. The review commit here (2361ee6) sits on a merge of #592's review head (8871a42), which merged clean, and was written as two failing tests first: test_a_set_carries_no_coefficient_of_its_own and test_writing_everything_out_reuses_the_curves_the_load_wrote_out.

Coverage, and what was left out

• The golden fixture carries both sets of coverage: feat(language): a model writes its formulations out on request, and a curve prints as the curve it states #582's three curves (three links under a gate every unit has; a bounded link under a points: mask and a gate only some units have; the hull), plus two method: lp curves — one masked by its own breakpoints, one over a whole axis bounded the other way — which are the only curves that reach the increasing, breakpoints and one-direction curvature arms.
• test_what_a_curve_assumes_of_its_numbers_rides_on_the_expansion_too is the load-time half of the invariant, and it is stronger than it was: to_program(spec).assumptions == to_program(spec.expand()).assumptions is now structural equality of predicates, so the text a load derives and the text the expansion emits have to agree exactly.
• test_every_check_has_a_sentence is parametrized over the four suffixes rather than over get_args(Check); test_a_curves_conditions_cannot_collide_with_a_written_assumption asserts the emitted-name collision rather than the retired space convention.
• test_a_method_names_the_curvature_it_is_exact_for gains a bounded method: convex case each way, and the pinned case keeps its answer under a new id.
• test_the_declared_bound_is_the_coefficient_rather_than_the_tighter_of_it_and_the_upper is gone with the key; test_a_set_carries_no_coefficient_of_its_own asserts the refusal and says why. The three fixtures that declared bound: 10 declare bounds.upper on the member instead.
• Walk._derived, _admitted and _parameter are gone with the union: an assumption is one line, whoever stated it.
• The how-to's seven Python values and six math lines were checked against a real run and a real render, and its YAML fence loads with python -m math_spec check.
• Left for a follow-up: no file under examples/ declares points:, so the masked curve — the one shape that emits all four conditions and the only one that derives parameters — has no worked example in the gallery. The YAML in the table is from a probe model rather than a committed one.
• Deliberately not done: the golden fixture gains no bounded method: convex curve. Its hull_curve is pinned both ways and its two lp curves already print the one-line comparison each way, so a fifth curve would print no form the document has not got.
• For the consumer to decide, not this PR: the predicate compares exactly. lpspec's validate_piecewise_data holds the bend against 1e-9 of the largest slope today, because an exactly collinear curve need not difference to exactly zero, and a cross-product scales as a product of differences rather than as a slope. Whoever runs these predicates over data settles what that tolerance is, and the language states none.
• Not done, on purpose: the lpspec side (a sink without a construct refuses the model and names spec.expand(), rather than rewriting it behind the author fluxopt/specsolve#1702) is the next change and waits on a release carrying Spec.expand. expand takes no per-kind options, and no inexact rewrite is admitted. The mutation table from feat(language): a model writes its formulations out on request, and a curve prints as the curve it states #582 was measured on its old base and is not restated here, because the guards it names have moved.

🤖 Generated with Claude Code

https://claude.ai/code/session_01CfY3asKSHvHahjNWxdDAER

https://claude.ai/code/session_019tCWoetBmjF1LpbTbjQY29

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34692569 | 📁 Comparing 75b0e91 against latest (bcf856c)

  🔍 Preview build  

29 files changed · + 3 added · ± 26 modified

+ Added

• howto/see-an-expansion/index.html
• reference/language/assumptions/index.html
• reference/math_spec/sos/index.html

± Modified

• about/limits/index.html
• about/what-counts-as-language/index.html
• examples/commitment/index.html
• howto/curve-by-hand/index.html
• howto/print/index.html
• reference/language/index.html
• reference/notation/index.html
• reference/reading/index.html
• reference/typeset/index.html
• reference/language/expressions/index.html
• and 16 more...