feat(language): a model writes its formulations out on request, and a curve prints as the curve it states

[FBumann]

Prompt: "Let’s implement the issue abou reformulation of sos and piecewise in mathspec. Does it depend on the assumptions or? If so, base it off of that"

and, each of which widened it: "As expanding a piecewise is now optional, we need a way of typesetting it o think. This should be included in this pr" · "A car with a parameter as a bound can simply use that parameter for the sos formulation, right?" → "Yes put it in the pr" · "I think we need all of this to work before we can merge this pr!!! … Blocked by the other 2 pts. We want to make the piecewise data checks part of the reformulation!"

Note

The following content was generated by AI.

Closes #579. Spec.expand() writes a formulation out on request, sos: is the second formulation, and the typesetter prints the block it was handed — spec.expand(), or --expand, prints the rows that block states.

Important

Blocked, and a draft until it is not. A curve's data contract is still a side channel: Program.piecewise[…].checks, which a consumer reads and words with check_message. It belongs in what the formulation states — assumptions: the expansion emits — so a written-out model carries its conditions as language, prints them in the document, and no consumer keeps a second mechanism for them. That needs the two PRs below, and then the work lands here before this merges.

• feat(language): a where may compare arithmetic over parameters #469 — a where compares arithmetic and parameter pairs. On this base where: "p_min <= p_max" is refused: "compares two parameters, which is not in the language", so no condition on breakpoints can be written at all.
• feat(language): a model declares what it assumes of its data, and the typeset math prints it #471 — assumptions:, Program.assumptions, assumption_message, and the Assumptions section of the typeset document.
• the expansion emits each piecewise: block's conditions as assumptions — <block> increasing, curvature, breakpoints, points — under the same rule the rest of this PR keeps: what a formulation emits, it derives.
• Check, check_message and PiecewiseDeclaration.checks retire, or the PR says which one stays and why.
• Contiguous is the one that does not map today: "the marked breakpoints are one run" needs a predicate that counts run starts. Either the grammar grows one, or that check stays and this PR says so.

On #471 as a dependency of what is already here: there is none. A set's two bound facts are decided at load from the declared bounds:, and a bound the data carries is a coefficient a row multiplies by rather than something the language has to know. assumptions appears nowhere in src/ on this base, so the branch is origin/main — and the block above is about the curve's conditions, not about anything in the diff.

What 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.
• 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: <set>_adjacency (order 2) or <set>_nonzero (order 1), each with a _below sibling. Every coefficient is read off the member's own bounds:, so a negative bound and one the data carries are both admitted; bound: replaces the one above where the file declares it, never the tighter of the two, which is the divergence a sink without a construct refuses the model and names spec.expand(), rather than rewriting it behind the author fluxopt/specsolve#1702 records. A coefficient that states nothing — a 1 above, a 0 below — is left out.
• method: adjacency is method: sos2 written out, so the binaries are spelled once, and big_m: is renamed bound:.
• The typesetter prints what it was handed — a piecewise: block is one line: the links on the locus through its breakpoints, conv for method: convex, the bounded link as a function of the pinned one, points: narrowing the breakpoints, an activity: as a factor. typeset no longer expands.
• Both readings are printable, with one symbol table — a table entry may name what a formulation emits, so the table that renames <block>_lam to λ renders the file it came from too. The three typeset verbs take --expand, because a shell cannot compose spec.expand(). The notation page shows every formulation twice: as the file states it, and as the rows it states.

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 blocked work finishes the same thought: a rewrite that is exact only under a condition should say that condition in the language, beside the rows it writes.

What breaks

• big_m: → bound:. 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 either bounds.upper, the set's bound:, or domain: binary. Each may be a parameter. A model whose member is unbounded on a side stops loading, because no row can pull an unpicked member back to zero from there.
• 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 — a constraint reading cost_curve_lam — is refused at load, because the load pass now resolves the file's own declarations as well as the expansion's.
• The pick row a gated method: adjacency curve emits is sum(seg, over=bp) <= 1 rather than == activity, and its second, ungated row is gone. The projection onto the author's own variables is unchanged — with the gate at 0 the convexity row pins every weight to 0 and the segment binaries reach nothing — so this is a looser integer formulation, not a different feasible set.
• Program.sos carries bound rather than big_m, and Resolved carries a piecewise field: each block's link expressions, typed, which is what lets the walk print a curve without expanding it.

Verified

Run in a uv venv (Python 3.12), because pixi is not installable in this environment:

• pytest -n 4: 1403 passed, none skipped — coverage is installed here, so the walk's line census runs, and every arm of the new curve print is reached by tests/typesetting/golden/model.yaml.
• ruff check, ruff format --check, pyrefly check, prettier --check on every .md/.yaml this branch touches: clean.
• python -m tools.render_tex: all 30 models render to standalone LaTeX.
• Generated artefacts regenerated and read: the schema, the three golden files, docs/reference/notation.md, the gallery pages, README.md and docs/index.md.
• The data contract survives every route: the Increasing, Curved and AtLeastTwo checks are identical on to_program(spec), to_program(spec.expand()) and to_program(spec.expand('sos')), pinned by test_what_a_curve_assumes_of_its_numbers_rides_on_the_expansion_too.

Not run: docs-build --strict — mkdocstrings fetches https://docs.python.org/3/objects.inv and this sandbox's proxy answers 403; compile-tex (no tectonic); reuse, typos, taplo, zizmor.

Mutation table

Each guard deleted in turn, the suite run, the file restored from a copy and the tree checked clean.

Guard	Caught by
the refusal of a member with no coefficient below	test_a_rule_decided_without_data[sos-over-a-member-with-no-floor]
the refusal of a member with no coefficient above	test_a_rule_decided_without_data[sos-over-a-member-with-no-coefficient]
the row below, at all	test_an_unpicked_member_is_held_at_zero_from_the_sides_its_bounds_state (the negative and the parameter case)
the row below written only where the bound states more	test_an_unpicked_member_is_held_at_zero_from_the_sides_its_bounds_state[a-member-that-starts-at-zero-needs-one-row], test_docs[notation]
the coefficient of 1 left out of a linking row	test_a_coefficient_of_one_is_left_out_of_the_row_rather_than_printed, test_docs[notation]
the collision check on a set's emitted names	test_a_rule_decided_without_data[sos-whose-expansion-collides-with-a-declaration]
to_yaml refusing an expansion that derived parameters	test_an_expansion_that_derived_parameters_prints_rather_than_round_trips
the refusal of a kind that is not a formulation	test_a_kind_this_language_does_not_have_is_refused_naming_both (both cases)
expand not storing a model that expands to itself	20 × TestTheFrontDoor::test_to_dict_reproduces_the_model, test_to_yaml_reproduces_the_model
a symbol table may spell what a formulation emits	test_one_table_spells_the_blocks_a_file_states_and_the_rows_they_state, test_docs[notation]
lowering refusing a model with a curve left in it	still green on the first run; test_lowering_refuses_a_model_that_still_owes_rows_to_a_curve added as the probe, and it fails with the guard deleted

Coverage moved, defaults departed from, and what was left out

• test_the_file_is_not_an_expansion_and_the_expansion_is and test_an_expansion_will_not_be_built_around_a_curve asserted the deleted type; their claims are now test_the_file_keeps_its_curve_and_the_expansion_has_none and the probe in the table above. test_a_name_declared_as_none_of_the_three_is_refused became ..._of_the_four_..., a curve being the fourth kind typeset_declaration prints.
• The sos-big-m-* validation cases are sos-bound-*. The two cases that refused a negative and a parameter-valued lower are gone with the rule: those models load now, and what they emit is asserted in test_sos.py's parametrized rows. sos-over-a-member-with-no-floor refuses the case that remains.
• test_boundedness's carried-by-a-set case had to become loadable: it declares bound: with bounds: {lower: 0} and no upper, which is the one shape that leaves a member of a set unbounded above, and is what that case needs.
• The golden fixture gains three curves — three links pinned, a bounded link under a masked gate and a points: mask, and the hull — so the operator census and the line census both reach the new print. The piecewise sidecar symbol tables stay, and name the weights again.
• Departed from the issue on three points, all named here rather than in the code. The issue rules out a flag; the command line gets --expand anyway, because a shell hands over a path and cannot compose spec.expand(). typeset_declaration accepts a piecewise: block's name, which the issue does not mention: a curve now prints as one line, so asking for that line by name is the same surface the other three kinds have. And the issue refuses a parameter-valued lower and defers it to feat(language): a model declares what it assumes of its data, and the typeset math prints it #471 — the second linking row makes it exact with nothing deferred, so it is admitted here instead.
• The issue scopes three PRs. They land here as one, because this session was given one branch; the three are separable and the commits are split along the seam.
• Still to come in this PR, per the block above: the curve's conditions as emitted assumptions:, once feat(language): a where may compare arithmetic over parameters #469 and feat(language): a model declares what it assumes of its data, and the typeset math prints it #471 are in.
• 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 math-spec release carrying Spec.expand and bound:. expand takes no per-kind options, typeset takes no expand= keyword, and no inexact rewrite is admitted.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QGvzXkPDrzi6f1PNmvebhc

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34663104 | 📁 Comparing 67d4966 against latest (bda1fc5)

  🔍 Preview build  

18 files changed · + 1 added · ± 17 modified

+ Added

• reference/math_spec/sos/index.html

± Modified

• about/limits/index.html
• about/what-counts-as-language/index.html
• howto/curve-by-hand/index.html
• howto/print/index.html
• reference/notation/index.html
• reference/reading/index.html
• reference/typeset/index.html
• reference/language/piecewise/index.html
• reference/math_spec/lowering/index.html
• reference/math_spec/model/index.html
• and 7 more...

[FBumann]

Superseeded by #602