feat(language): a model declares what it assumes of its data

[FBumann]

Prompt: Lets rebase #471 onto 566

And rethink the architecture!

Prompt: Do the description change

Prompt: "Review the stack of 602 and below" — "Do 1-3"

Note

The following content was generated by AI.

Replaces #471, which is stacked on the retired #469. A file states what it
assumes of its data under assumptions:. Program.assumptions is the one
place a consumer reads every fact the numbers must meet, the file's and each
curve's, with one message function.

What this changes

Surface. An eleventh declaration key, assumptions:. An entry is a bare
where string, or a mapping with holds:, an optional where: and a
description:. It holds at every coordinate of the product of the dimensions
its two masks name, a missing row reading as false as in any where. There is
no dims:, because a predicate widens nothing. A predicate that folds to a
literal is refused, and so is a where: that folds to one: true narrows
nothing, and false checks the entry on no row. A variable in either is
refused. Reference: docs/reference/language/assumptions.md.

An assumption is named outside the flat namespace, as a constraint is:
no expression names either, so a model may name an assumption after a
variable. The expressions page says so beside the sentence on constraints.
typeset_declaration refuses a name declared as two of the kinds it prints,
as it did for a constraint and a variable.

One carrier for what the data has to satisfy. Program.assumptions maps a
name to an Assumption: the file's entries as Holds(predicate, where, description), then each piecewise: block's own conditions, in block order.
PiecewiseDeclaration.checks is gone, and check_message is
assumption_message. Increasing and Curved now carry the method their
sentence quotes, and all four derived members carry their block, so the
sentence needs no second argument. A derived entry is named
<block> increasing; the space is what keeps the two kinds apart in one
mapping, since a declaration is named the way an expression writes it and no
file can write that name.

The author's words reach the refusal. A description: says why a rule is
there, which the parameter names do not. Holds carries it, and
assumption_message trails the sentence with it, so a failure names the
columns that are wrong and the reason the rule exists. This is what #268 asked
its refusals: block for, under message:.

Rendering. A fourth section, Assumptions, after Variable domains: each
entry as a line, a lone comparison aligned on its relation as a constraint is,
then each curve's conditions. The increasing x-axis is an inequality between
neighbours under the plain translation; the shape a method is exact for is
prose, as a paper writes it; the two conditions on a points: mask are stated
of the set the mask admits. Format.set_of is the one new format method.
typeset_declaration takes an assumption name, and the notation page shows
what each method: row assumes.

Why

An assumption about the numbers is a rule two engines must not answer
differently, so it is language; the numbers are the engine's, so the engine
checks. The language already did this once, for piecewise:, under a second
vocabulary. Landing the author's entries beside those rather than next to them
leaves a consumer with one mapping, one closed union and one refusal sentence.

What the port dropped, and why this is not a rebase

#471 forked at alpha.91; main is alpha.108. Merging #566's branch into
it conflicts in 27 of the 36 files it touches, so the change is re-applied
here rather than replayed — the hard rule is never to force-push.

#471's centre was ParameterPairComparisonNode, built because #469 admitted
p_min <= 0.5 * p_max and refused p_min <= p_max. #566 deletes that
refusal, so the node goes, with its dtype refusal, its param_pair
exclusivity subject and _PAIR_ORDERS, its dimension rule, its schema entry
and its typesetter branch. p_min <= p_max lowers as an
ExpressionComparison like any other arithmetic. A case when: cannot
compare two parameters, which is #566's rule for every comparison of
expressions, not a loss this PR adds.

Gates

pixi is refused by this environment's egress proxy, so the gates ran from a
uv environment on Python 3.12. That is a departure from the "everything runs
in a pixi environment" default.

gate	result
pytest -n 4	1426 passed, 1 skipped (#566's head: 1398 passed, 1 skipped)
ruff check, ruff format	clean, on the pinned 0.16.1
pyrefly check	0 errors
typos, reuse lint	clean before the review commit; not run for it
prettier --check	clean before the review commit; not run for it
mkdocs build --strict	clean, with the docs.python.org inventory dropped for the run, which the proxy refuses with 403
render-tex	30 models rendered
compile-tex	not run, for want of a TeX distribution

The schema, the three golden files, the notation page and the gallery pages
were regenerated and read. Both YAML models on the new page load with
python -m math_spec check. The description commit regenerates none of them:
it changes no typeset output, so the goldens and the generated pages are byte
for byte what the suite already held.

The review commit (3352776) was written as three failing cases first, in
TestAssumptions: a-where-that-is-always-false,
a-where-that-hides-a-variable-behind-a-fold and
a-where-that-is-always-true. The merge of #566's review commit is its own
commit (7e9f7a6), resolving one conflict in tests/test_lowering.py by
keeping both sides.

Mutation table

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

Guard	Caught by
the literal-fold refusal	TestAssumptions[a-predicate-that-is-always-true], [...-always-false]
the where-fold refusal	TestAssumptions[a-where-that-is-always-false], [...-always-true], [...-behind-a-fold]
the variable refusal	TestAssumptions[a-variable-in-the-predicate], [a-variable-in-the-where]
the derived entries in Program.assumptions	test_assumptions_carry_the_file_s_entries_and_the_curves_behind_them, 9 more in test_piecewise
the Assumptions section in the walk	the three golden files, the notation page and gallery:commitment.md
the description on Holds	test_an_assumption_refuses_in_the_words_the_file_wrote, test_the_page_shows_the_declarations_the_expansion_emits
the description in the sentence	the same two

The walk's line census was the guard that caught the two arms the fixture did
not reach while this was being written: line() for an assumption, and the
assert_never on the derived union.

Coverage moved, and what was left out

• test_a_block_is_kept_as_the_checks_a_consumer_binding_it_runs is
  test_a_block_assumes_of_its_data_what_the_method_implies, asserting the
  whole Program.assumptions mapping rather than a checks tuple.
• test_every_check_has_a_sentence reads the mapping and calls
  assumption_message; test_a_method_names_the_curvature_it_is_exact_for
  and test_a_file_supplied_mask_derives_nothing read it too.
• test_a_name_declared_as_none_of_the_three_is_refused is
  ..._of_the_four_....
• tests/test_reading_page.py checks 16 claims rather than 12: the page's new
  block is run like the rest of it, and curve.yaml gains one written
  assumption so the refusal quoting its description: is a line the suite
  evaluates.
• The golden fixture gains a bp dimension, two lp curves — one masked by
  its own breakpoints, one over the whole axis — and eight assumptions, so
  every new arm of the walk prints into a committed file.
• Not done, on purpose: the lpspec side — evaluating Program.assumptions
  at the data door — is its own PR, as feat(language): a where may compare arithmetic over parameters #566 said of the mask evaluator. The
  typeset document prints no description:, for an assumption as for a
  constraint: where author prose belongs in an equation is one question for
  every declaration, and answering it for this key alone puts a paragraph
  inside a math line. The convex method's "convex or concave" wording is
  reached through the notation page rather than the golden fixture, which
  would have cost a third curve for one string. An empty description: ""
  loads and says nothing; refusing it is one field constraint, left for a
  reviewer to ask for.

A limit moved. docs/about/limits.md said a check on a column belongs in
data preparation. It now says the rule is language and the check is the
consumer's, and the unit-checking row points at assumptions: for a range.

🤖 Generated with Claude Code

https://claude.ai/code/session_018YVS5Ngm3dvMzrYw6sFwbz

https://claude.ai/code/session_019tCWoetBmjF1LpbTbjQY29

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34692251 | 📁 Comparing 3352776 against latest (11a8a2e)

  🔍 Preview build  

25 files changed · + 1 added · ± 24 modified

+ Added

• reference/language/assumptions/index.html

± Modified

• CHANGELOG/index.html
• about/limits/index.html
• examples/commitment/index.html
• reference/language/index.html
• reference/notation/index.html
• reference/reading/index.html
• reference/typeset/index.html
• reference/language/expressions/index.html
• reference/language/file/index.html
• reference/language/piecewise/index.html
• and 14 more...