Record ratified rulings

conformance/JUDGMENT_CALLS.md

@@ -1,13 +1,15 @@
 # JUDGMENT_CALLS — semantic decisions awaiting ratification
 
-Every section below is a semantic question the interpreter currently
-answers by accident of implementation. Nothing here is ratified. Each
-section states the question, what `js/mpl.js` observably does today, and
-which corpus entries pin that behavior. The `RULING:` line is blank on
-purpose — rulings are Reverend's, in Stage 3, in batches. A ruling either
-blesses the observed behavior (the pinning entries flip to `ratified`) or
-overrules it (the interpreter changes, the entries are re-recorded, then
-ratified).
+RATIFIED 2026-07-09 — this file is the semantic record of MPL M0.
+
+Every section below is a semantic question Stage 2 surfaced, stated with
+the behavior `js/mpl.js` exhibited at observation time (Stage 2 head,
+`ea66a2a`) and the corpus entries that pinned it. Each `RULING:` line
+records Reverend's ratified decision of 2026-07-09. BLESS rulings kept the
+observed behavior; OVERRIDE/SPLIT/IMPLEMENT/AMEND rulings changed the
+grammar or the interpreter in Stage 3, and the corpus was re-recorded to
+match. The "Observed:" text is the historical record, not the current
+behavior — the rulings govern.
 
 ## 1. Division by zero
 
@@ -15,7 +17,7 @@ Question: what does `x ÷ 0` do — error, infinity, or ⊥?
 Observed: raises `err_div0` (both `÷` and `/`, integer or float operands).
 Pins: `043_div_zero`.
 
-RULING:
+RULING: BLESS. `x ÷ 0` (and `/`) raises `err_div0`. Division by zero is undefined.
 
 ## 2. The value of a ∀ expression
 
@@ -23,7 +25,7 @@ Question: what does `∀ x ∈ list : body` evaluate to?
 Observed: the value of the last body evaluation; `⊥` for an empty list.
 Pins: `018_forall_value`, `019_forall_scope`.
 
-RULING:
+RULING: OVERRIDE. `∀` is an iterator; the expression's value is `⊥` always (including empty collections). Using a statement as a value is undefined — same principle as ruling 3.
 
 ## 3. Result when no guard matches
 
@@ -32,7 +34,7 @@ Observed: an internal no-match that surfaces as `⊥` everywhere except
 directly to the left of `|`.
 Pins: `021_no_guard_match`, `023_alt_chain`.
 
-RULING:
+RULING: BLESS (semantics, not mechanism). An unmatched guard yields `⊥` unless caught by `|`. Implementations choose their own internal sentinel.
 
 ## 4. Integer vs float display
 
@@ -43,7 +45,7 @@ decimal point (`2`), non-integral as JS renders them (`0.5`, and
 `0.50` → `0.5`).
 Pins: `006_number_display`, `007_float_arithmetic`.
 
-RULING:
+RULING: OVERRIDE. Numbers are exact rationals (arbitrary-precision integer numerator/denominator). Decimal literals convert exactly (`0.1` = 1/10). Display: integers bare; otherwise lowest-terms fraction `num/den`, sign on the numerator, denominator > 0; zero as `0`. Output is valid MPL that re-evaluates to the same value. IEEE doubles are rejected: the language must not lie about `0.1`. `√ vs ℚ` is logged as a standing M1 decision.
 
 ## 5. ✎ formatting per type
 
@@ -53,7 +55,7 @@ quoted inside lists; booleans `true`/`false`; lists `[a, b]` with
 one-space separation; closures as `λ`; `⊥` as `⊥`.
 Pins: `009_string_concat`, `011_list_display`, `031_show_all_types`.
 
-RULING:
+RULING: BLESS, spec'd. `✎` renders: numbers per ruling 4; strings bare at top level, double-quoted inside lists; booleans `true`/`false`; lists `[a, b]` (comma-space); closures as `λ`; `⊥` as `⊥`.
 
 ## 6. ⊥ display and propagation
 
@@ -63,7 +65,7 @@ strings (`"x" + ⊥` → `x⊥`), sits in lists, but arithmetic on it is
 `err_num`.
 Pins: `030_bot`, `052_bot_arith`.
 
-RULING:
+RULING: BLESS. `⊥` is first-class: displays as `⊥`, sits in lists, string concatenation renders it (`"x" + ⊥` → `x⊥`); arithmetic on it is `err_num`.
 
 ## 7. Equality across types
 
@@ -74,7 +76,7 @@ and `⊥ = ⊥` → `true`. Comparing a self-referential closure crashes with a
 keyless host error (unpinnable by the corpus).
 Pins: `034_cross_type_equality`, `033_string_compare`.
 
-RULING:
+RULING: SPLIT. Data equality is structural: element-wise lists, cross-type `=` is `false`, `⊥ = ⊥` is `true`, `0.5 = 1/2` is `true` (same rational). Any equality comparison involving a function raises `err_fn_eq` — function equality is undecidable; a keyed error replaces the current keyless crash.
 
 ## 8. Ordering across types
 
@@ -83,7 +85,7 @@ Observed: raw host comparison with JS coercion — `1 < "2"` → `true`,
 `"10" < 9` → `false`, `true < 2` → `true`; strings order lexicographically.
 Pins: `035_mixed_compare`, `033_string_compare`.
 
-RULING:
+RULING: OVERRIDE. `< > ≤ ≥` are defined on number×number and string×string (Unicode code-point order) only; anything else raises `err_compare`. Host coercion (`1 < "2"`) is JavaScript soul leakage, not mathematics.
 
 ## 9. Closure capture
 
@@ -93,7 +95,7 @@ Observed: the environment — later mutation of a captured variable is
 visible on the next call (`013` prints 11 then 21).
 Pins: `013_closure_capture`, `026_def_vs_assign_scope`.
 
-RULING:
+RULING: BLESS. Closures capture the environment. (The corpus itself forces this: `factorial` only works because the λ sees its own later binding.)
 
 ## 10. Recursion depth
 
@@ -104,7 +106,7 @@ before the 500 000-step budget can trigger, so the corpus cannot pin it
 `err_steps`. Depth ~500 is comfortably safe.
 Pins: `016_recursion_sum` (works at 500), `053_step_budget` (`err_steps`).
 
-RULING:
+RULING: OVERRIDE. Recursion is bounded by an explicit λ-application depth counter, limit 10 000, raising `err_depth`. A keyless host RangeError is a hole in the error surface; the limit is conformance surface in every implementation.
 
 ## 11. The step budget itself
 
@@ -114,7 +116,7 @@ Observed: hard-coded 500 000; nested `∀` loops over a 10-element list six
 deep exceed it.
 Pins: `053_step_budget`.
 
-RULING:
+RULING: RECLASSIFY. The step budget is an environment resource limit, not language semantics — like out-of-memory. `err_steps` (500 000) remains in the browser implementation; entry 053 leaves the portable corpus and becomes a js/test implementation test.
 
 ## 12. String escape round-tripping
 
@@ -125,7 +127,7 @@ grammar instead REJECTS unknown escapes — a recorded divergence.
 Pins: `008_string_escapes`; divergence in DIVERGENCES.md ("drop\qme" and
 the `"a\zb"` fuzz entry).
 
-RULING:
+RULING: OVERRIDE. Escapes are exactly `\n \t \" \\`; any other `\x` raises `err_escape`, matching the grammar. Silent data-mangling is forbidden.
 
 ## 13. Guard condition truthiness
 
@@ -135,7 +137,7 @@ strings, lists and `⊥` do not (they yield the no-match path) — so numbers
 are truthy for `⟹` but nothing else is.
 Pins: `022_guard_truthiness`.
 
-RULING:
+RULING: OVERRIDE. A guard condition must be boolean; any non-boolean condition (numbers included) raises `err_bool`. A condition is a proposition.
 
 ## 14. ∧ ∨ operand truth
 
@@ -146,7 +148,7 @@ Observed: no — operands are tested with strict boolean equality, so
 accident in the surface.
 Pins: `036_logic_ops`, `037_logic_short_circuit`.
 
-RULING:
+RULING: SPLIT. `∧ ∨` short-circuit (blessed, observable by side effect) and demand boolean operands — a non-boolean evaluated operand raises `err_bool` instead of silently comparing false. One notion of truth, everywhere; an unevaluated right operand raises nothing.
 
 ## 15. Block scoping
 
@@ -155,7 +157,7 @@ Observed: no — bindings made inside a brace block leak out (`028` prints
 9). Only λ bodies and each `∀` iteration scope.
 Pins: `028_block_no_scope`, `027_block_sequencing`.
 
-RULING:
+RULING: BLESS. Braces group; they do not scope. Scope is created by binders only (λ parameters, ∀ iteration variables) — the Curry-Howard reading: a discharged hypothesis IS a λ. An explicit local-binding construct (let/where) is logged as a standing M1 decision.
 
 ## 16. ≜ vs ← scoping and creation
 
@@ -168,7 +170,7 @@ legal re-definition).
 Pins: `024_def_assign_rebind`, `025_def_assign_value`,
 `026_def_vs_assign_scope`.
 
-RULING:
+RULING: OVERRIDE (both halves). `≜` introduces a name exactly once per scope — same-scope redefinition raises `err_redef`; shadowing in inner scopes is legal. `←` mutates the nearest enclosing binding and raises `err_unbound` when none exists — silent creation is the typo trap. Both remain expressions returning the value.
 
 ## 17. Type constraints
 
@@ -178,7 +180,7 @@ is discarded unevaluated — `g ≜ λs∈𝔹: s + "!"` happily takes a string.
 Matches the site's "parsed today, not yet enforced" claim.
 Pins: `039_type_constraint_unenforced`.
 
-RULING:
+RULING: BLESS. Type constraints parse and are discarded, unenforced — this is the published claim and Stage 5's mandate.
 
 ## 18. Nullary calls and zero-parameter λ
 
@@ -188,7 +190,7 @@ so every `f()` is a runtime `err_arity`. The call syntax exists; nothing
 can satisfy it.
 Pins: `046_arity_nullary`, `047_arity_extra`.
 
-RULING:
+RULING: AMEND GRAMMAR. Nullary functions exist: `λ: e` is admitted (bare colon; the parenthesized spelling stays rejected per ruling 25). Effects made M0 procedural the day `✎` entered it; arity 0 is not an exception to ℕ. `f()` calls it; arity mismatches remain `err_arity`.
 
 ## 19. ∗ as multiplication
 
@@ -196,7 +198,7 @@ Question: is `∗` (U+2217) an operator, and what does it mean?
 Observed: exactly `×` — same token, same precedence.
 Pins: `041_asterisk_multiplication`.
 
-RULING:
+RULING: BLESS. `∗` (U+2217) is exactly `×`.
 
 ## 20. Divergence: empty program
 
@@ -206,7 +208,7 @@ Observed: the grammar accepts it; the JS interpreter rejects it
 Pins: none possible until ruled (decision 3 — divergent programs cannot
 enter the corpus). Repro in DIVERGENCES.md (fuzz index 49).
 
-RULING:
+RULING: OVERRIDE. The empty program is valid and produces no output. The grammar is right; the interpreter accepts it.
 
 ## 21. Divergence: sequences inside parentheses
 
@@ -217,7 +219,7 @@ rejects both (`err_expect`).
 Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 86, 119,
 247, 233, 279, 406, 468, 101…).
 
-RULING:
+RULING: OVERRIDE. Parentheses contain one seqExpr per the standing DECISIONS ruling: `(e1; e2)` is legal, value = last expression. The interpreter implements its own language.
 
 ## 22. Divergence: `∘` composition
 
@@ -227,7 +229,7 @@ even has the `\circ` escape) but has no parse rule for it — every use is
 `err_expect`.
 Pins: none until ruled. Repro in DIVERGENCES.md (fuzz index 9).
 
-RULING:
+RULING: IMPLEMENT. `∘` is function composition: `(f ∘ g)(args…) = f(g(args…))`. Operands must be functions — a non-function operand raises the expected-a-function key (reuse the existing key if the audit finds one, else introduce `err_fn`). Precedence and associativity follow the grammar.
 
 ## 23. Divergence: set literals
 
@@ -237,7 +239,7 @@ Observed: the grammar accepts `({5, "a b"})` and friends; the JS
 interpreter has no set support and rejects them (`err_expect`).
 Pins: none until ruled. Repros in DIVERGENCES.md (multiple fuzz indexes).
 
-RULING:
+RULING: PARSE-ONLY. Set literals parse (the interpreter gains the grammar's brace disambiguation) and evaluation raises `err_notyet`. Set semantics are an M1 design, logged.
 
 ## 24. Divergence: record literals
 
@@ -248,7 +250,7 @@ Observed: the grammar accepts `({y: 0})`; the JS interpreter rejects
 Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 25, 212,
 425, 427, 447).
 
-RULING:
+RULING: PARSE-ONLY. Record literals: same as 23.
 
 ## 25. Divergence: parenthesized λ parameters
 
@@ -260,7 +262,7 @@ The interpreter carries a syntax form the language explicitly rejected.
 Pins: none until ruled. Repros in DIVERGENCES.md (fuzz indexes 13, 29,
 76, …).
 
-RULING:
+RULING: OVERRIDE. `λ(a, b): e` is rejected by the interpreter too — the grammar already enforces the ratified DECISIONS ruling.
 
 ## 26. Divergence: bare λ and Greek letters as identifiers
 
@@ -271,4 +273,4 @@ Observed: grammar accepts `({λ})`; JS rejects (`err_expect` — λ demands a
 parameter list).
 Pins: none until ruled. Repro in DIVERGENCES.md (fuzz index 52).
 
-RULING:
+RULING: AMEND GRAMMAR. `λ` is a reserved token, never an identifier. Only λ; other Greek letters (π et al.) remain identifiers — Fatima wants π.