feat(language): a model states the conditions its data must satisfy, so a table that breaks one is refused rather than solved

[FBumann]

Prompt: "How would we implement this? / As part of the program? / And what about typesetting?" → "Lets do a Draft PR for this. Implement it in the best and easiest way!"

Note

The following content was generated by AI.

What this changes

checks: declares a where predicate the bound data must satisfy. It builds no row and changes no answer — it is the sentence a reader has to believe about the table before believing the constraints above it.

checks:
  omega_is_a_share: "CVaR_omega >= 0 AND CVaR_omega <= 1"
  efficiency_is_a_share:
    holds: "Link_efficiency > 0 AND Link_efficiency <= 1"
    description: a link delivers some of what it takes, and no more

No foreach. The frame is read off the predicate's own names, so a check is asked at every coordinate they span and a scalar one is a single question.

Why the vocabulary is the one that was already there

origin/main already carries a Check union — Increasing, Curved, AtLeastTwo, Contiguous — and check_message, for what a piecewise: block assumes of its curve. A declared condition is the same fact with a different provenance, so Holds joins that union rather than starting a second one: a consumer dispatches on one closed set whether a curve implied the condition or the file wrote it.

That cost two small reshapes, flagged because they edit code #237 landed:

• check_message(block, pw, check) → check_message(context, check). The pw argument existed only to reach pw.method, so Increasing and Curved now carry the method their own sentence names, and the function is a pure dispatch on the check.
• tests/test_piecewise.py::test_every_check_has_a_sentence sweeps get_args(Check), so it demanded a sentence for Holds the moment it joined — it now sources checks from both provenances.

And it typesets

A construct the loader admits, the typesetter renders. Walk.where() already renders any predicate in all three formats, so this is a Walk.checks() and a fourth section; no new rendering code. examples/pypsa_stochastic.yaml, in markdown:

#### Data conditions

**`omega_is_a_share`**

$$\mathrm{CVaR}^{\mathrm{omega}} \ge 0 \wedge \mathrm{CVaR}^{\mathrm{omega}} \le 1$$

**`tail_probability_is_one_or_more`**

$$\mathrm{CVaR}^{\mathrm{inv,tail}} \ge 1$$

A check over a dimension carries the quantifier its own names span — $$\mathrm{p}^{\mathrm{max}}_{g} > 0 \wedge \mathrm{eta}_{g} \le 1 \qquad \forall\thinspace g \in \mathcal{G}$$ — and a scalar one carries none.

It is a section a page may leave out, like the legend: typeset(..., checks=False) and --no-checks. A condition on the input is not a row a solver holds, so a page about the math alone drops it, and the rest is byte-identical to the same model with no checks at all (asserted, in test_the_data_conditions_are_left_out_on_request).

What is decided at load, and what is not

No file determines whether a table satisfies a condition — the consumer binding the data raises it, in the language's own words (check_message), the shape #242 established. What the file can decide, it does:

refused at load	why
a predicate the connectives settle to True	checks nothing
one they settle to False	refuses every table
one reading a variable	a check is settled before any variable has a value

What crosses the boundary

Two things, and nothing comes back — this repo never holds data, so there is no result type to own:

program.checks['omega_is_a_share']
# Holds(holds=<resolved WhereNode>, dims=(), description='the objective blends ...')

check_message("check 'omega_is_a_share'", holds)
# "check 'omega_is_a_share': the data does not satisfy it — the objective blends the
#  expectation and the tail at `omega` and `1 - omega`, so outside [0, 1] it is an
#  extrapolation of the two rather than a mix of them"

The consumer evaluates the predicate over dims and raises that sentence with its own account of what it saw — the shape check_message has had since #237, and the division #242 established.

A check is the one declaration whose prose reaches the program. reading.md says a program cannot answer what the file wrote, and this is the exception it now names: for every other declaration a description: is for the typeset page, and here it is the second half of the refusal. Without it a consumer holding only the program prints the check's name and nothing about why it matters.

Severity stays prose. Nothing carries "error or warning", exactly as coverage: carries none — the must is the declaration, and #243 has lpspec raise a DataError on the strength of the reference alone. What the failing coordinates look like is the consumer's, by the second edge of what-counts-as-language.

Verified

pixi run ci on this branch — lint, test (839 passed, 828 on the base — 11 new), docs-build --strict, compile-tex (26 documents, the stochastic example among them). schema/math-spec.schema.json and tests/typesetting/golden/*.out regenerated by their own tools.

Mutation table

Each guard deleted in turn on a clean tree, restored with git checkout --:

Mutation	Result
the variable refusal never fires	2 failed
the always-true arm is dropped	2 failed
the never-true arm is dropped	2 failed
restored	839 passed

The always-true arm is the one that matters: without it a check that holds whatever the data says reaches _lower_check's assertion instead of a load error, which is the failure mode #223 was about.

tests/typesetting/test_golden.py::test_the_golden_model_reaches_every_line_of_the_walk also refused the first version — Walk.checks() was five unreached lines until the golden model declared two, one over a dimension and one scalar, so both quantifier branches print.

The evidence this rests on

Sorted every parameter across the seven example models. The conditions that matter there are relational or reductive, not scalar ranges — which is why this is a predicate block and not minimum:/maximum: attributes:

condition	where	expressible here
0 <= CVaR_omega <= 1	pypsa_stochastic.yaml	yes — added in this PR
CVaR_inv_tail >= 1	pypsa_stochastic.yaml	yes — added in this PR
Link_efficiency is a share	every PyPSA model	yes
Line_loss_offset < 0 (prose only today)	pypsa_losses.yaml	yes
Generator_p_min_pu <= Generator_p_max_pu	5 models	no — needs a parameter-to-parameter comparison
sum(scenario_weight, over=scenario) == 1	pypsa_stochastic.yaml	no — needs a reduction in a predicate

pypsa_stochastic.yaml:9 says "the cost is the expectation over the scenarios' weights", and nothing enforces that they sum to one. That row is the strongest case for the feature and it is the one that has to wait.

Deliberately not done

No parameter-to-parameter comparison. holds: "Generator_p_min_pu <= Generator_p_max_pu" is refused today by resolution.py, and widening that is lpspec#851 — already decided yes upstream, with its own ledger rows in examples/pypsa.yaml (Generator_partly_tightened, Generator_must_stay_up). Separate PR, separate decision.

No reduction in a predicate. The sum-to-one row needs one, and the dim-algebra reason a where: cannot reduce (lpspec#469) may not apply to a check, whose output shape is stated rather than inferred. Worth deciding on its own rather than behind this.

No enforcement here, because there is nothing to enforce without data. No entry in the ten rules — a check states no rule about what the model means, and whether the front door's table should mention it is an editorial call that is yours.

Draft, because the two rows above are the ones that justify the block, and you may want them settled before this lands.

Closes #268

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34306945 | 📁 Comparing 2ba5161 against latest (a9237ec)

  🔍 Preview build  

11 files changed · ± 11 modified

± Modified

• reference/typeset/index.html
• reference/language/declarations/index.html
• reference/language/file/index.html
• reference/language/reading/index.html
• reference/math_spec/dimensions/index.html
• reference/math_spec/lowering/index.html
• reference/math_spec/model/index.html
• reference/math_spec/piecewise/index.html
• reference/math_spec/program/index.html
• reference/math_spec/validation/index.html
• and 1 more...

[FBumann]

Superseeded by #471