From 10d620cc0cce86ef1f3e835efb4a8073d5c24d17 Mon Sep 17 00:00:00 2001
From: lex00 <121451605+lex00@users.noreply.github.com>
Date: Wed, 7 Oct 2026 21:41:12 -0600
Subject: [PATCH] spec: rewrite the prose the sentences 0.5.1 rules flag, and
 drop its baseline entries

The 107 baselined findings in spec/*.md are gone: repeated openings,
conjunction openers, epistrophe, comma series, colon nameplates and two
em dashes. Sentences are reordered or merged; rule identifiers, defined
terms and MUST/SHOULD conditions are unchanged. Three inline lists became
tables. The spec baseline is now empty (191 -> 84 overall).
---
 scripts/docs-sentences-baseline.json |  67 ----------------
 spec/CHANGELOG.md                    |  10 +--
 spec/README.md                       |  95 ++++++++++++-----------
 spec/divergence.md                   |  11 ++-
 spec/grammar.md                      |  50 +++++++-----
 spec/hosts.md                        |  69 ++++++++++-------
 spec/inventory.md                    |  14 ++--
 spec/judgments.md                    |   8 +-
 spec/prior-art.md                    |  35 ++++-----
 spec/rationale.md                    | 112 +++++++++++++++------------
 spec/rules.md                        |   6 +-
 spec/taint.md                        |  53 +++++++------
 spec/values.md                       |  25 +++---
 spec/verdict.md                      |   6 +-
 14 files changed, 269 insertions(+), 292 deletions(-)

diff --git a/scripts/docs-sentences-baseline.json b/scripts/docs-sentences-baseline.json
index d1c6bc6..023144c 100644
--- a/scripts/docs-sentences-baseline.json
+++ b/scripts/docs-sentences-baseline.json
@@ -1,71 +1,4 @@
 {
- "spec/CHANGELOG.md": {
-  "anaphora/repeated-opening": 2
- },
- "spec/README.md": {
-  "anaphora/repeated-opening": 11,
-  "discourse/conjunction-opener": 3
- },
- "spec/divergence.md": {
-  "tricolon/comma-series": 2,
-  "discourse/conjunction-opener": 1,
-  "anaphora/repeated-opening": 1
- },
- "spec/grammar.md": {
-  "anaphora/repeated-opening": 5,
-  "tricolon/comma-series": 2,
-  "discourse/punchy-fragments": 2,
-  "discourse/epistrophe": 1,
-  "tricolon/density": 1,
-  "discourse/conjunction-opener": 1
- },
- "spec/hosts.md": {
-  "anaphora/repeated-opening": 7,
-  "claude/colon-reveal": 3,
-  "tricolon/comma-series": 3,
-  "discourse/epistrophe": 1,
-  "discourse/conjunction-opener": 2
- },
- "spec/inventory.md": {
-  "tricolon/comma-series": 1,
-  "anaphora/repeated-opening": 2
- },
- "spec/judgments.md": {
-  "discourse/epistrophe": 1,
-  "anaphora/repeated-opening": 1
- },
- "spec/prior-art.md": {
-  "anaphora/repeated-opening": 6,
-  "discourse/epistrophe": 2,
-  "discourse/conjunction-opener": 1,
-  "tricolon/comma-series": 1
- },
- "spec/rationale.md": {
-  "anaphora/repeated-opening": 16,
-  "discourse/conjunction-opener": 3,
-  "tricolon/comma-series": 4,
-  "tricolon/density": 1,
-  "discourse/punchy-fragments": 2
- },
- "spec/rules.md": {
-  "tricolon/comma-series": 1
- },
- "spec/taint.md": {
-  "tricolon/comma-series": 4,
-  "formatting/em-dash-density": 2,
-  "anaphora/repeated-opening": 2,
-  "discourse/conjunction-opener": 1,
-  "discourse/epistrophe": 1
- },
- "spec/values.md": {
-  "anaphora/repeated-opening": 3,
-  "discourse/conjunction-opener": 1,
-  "tricolon/comma-series": 1
- },
- "spec/verdict.md": {
-  "anaphora/repeated-opening": 1,
-  "tricolon/comma-series": 1
- },
  "paper/discussion.md": {
   "discourse/epistrophe": 1,
   "anaphora/repeated-opening": 1
diff --git a/spec/CHANGELOG.md b/spec/CHANGELOG.md
index bc2e349..2e80fce 100644
--- a/spec/CHANGELOG.md
+++ b/spec/CHANGELOG.md
@@ -1,6 +1,6 @@
 # Changelog
 
-The versioned history of the rule set. The policy is in [`README.md`](./README.md) under "Versioning". A version names a set of rules, `S-*` and `F-*` with their normative text, and nothing else: not a chant release, not a revision of the rationale. The current version is the single line in [`VERSION`](./VERSION).
+The versioned history of the rule set. The policy is in [`README.md`](./README.md) under "Versioning". A version names a set of rules, `S-*` and `F-*` with their normative text, and nothing else: not a chant release, not a revision of the rationale. The single line in [`VERSION`](./VERSION) holds the current version.
 
 Each entry lists the rules that changed and how in the four kinds the policy defines. A change confined to non-normative text is not versioned and is not listed here; the rationale sections and the inventory are the usual cases.
 
@@ -55,10 +55,10 @@ F-Rule-Finding already carries the result to the author.
 
 Item 1 named what an entity *carries* and never what constructing one may
 *do*, so a host could put a validating, graph-building constructor behind it
-and violate no rule. Folding invokes that constructor through revival
-(F-Val-Fate). Item 1 was the one place code runs during a fold with nothing
-said about it: F-Host-Admission bounds an intrinsic and F-Rule-Pure bounds a
-rule. #203 made F-Host-Admission's clause observable and left this
+and violate no rule. Since folding invokes that constructor through revival
+(F-Val-Fate), item 1 was the one place code runs during a fold with nothing
+said about it: F-Host-Admission bounds an intrinsic and F-Rule-Pure bounds
+the code a rule runs. #203 made F-Host-Admission's clause observable and left this
 half of #173 open. This closes it.
 
 The bound was already implicit in the construction form item 1 names. A class
diff --git a/spec/README.md b/spec/README.md
index 1eea3b1..5e1a471 100644
--- a/spec/README.md
+++ b/spec/README.md
@@ -5,27 +5,29 @@ one rule set.
 
 **At a fixed build-parameter binding folding a file and running it are
 observationally equivalent.** That is the objective every rule here serves.
-[`objective.md`](./objective.md) states it with the two profiles an
+The file [`objective.md`](./objective.md) states it with the two profiles an
 implementation may claim and the notation the judgments are written in. Start
 there.
 
 The rules in reading order:
 
-- [`grammar.md`](./grammar.md) (`S-*`) the grammar of the fold subset.
-- [`evaluation.md`](./evaluation.md) (`F-Eval-*`) J1 expression evaluation.
-- [`verdict.md`](./verdict.md) (bare `F-*`) J2 the per-file verdict.
-- [`taint.md`](./taint.md) (bare `F-*`) J3 the identity-taint fixpoint.
-- [`observables.md`](./observables.md) (`F-Obs-*`) J4 properties and observables.
-- [`values.md`](./values.md) (`F-Val-*`) the value domain.
-- [`divergence.md`](./divergence.md) (`F-Direction`, `F-Div-*`, `F-Exc-*`) divergence between the shape classifier and the folder.
-- [`hosts.md`](./hosts.md) (`F-Host-*`) the host interface.
-- [`rules.md`](./rules.md) (`F-Rule-*`) rules over values.
-
-[`judgments.md`](./judgments.md) indexes J1 through J4.
-
-Nothing in the three appendices is normative.
-[`rationale.md`](./rationale.md) carries the reasoning that motivated each
-rule. [`inventory.md`](./inventory.md) is the coverage ledger. Every decision
+| File | Identifiers | Contents |
+|---|---|---|
+| [`grammar.md`](./grammar.md) | `S-*` | the grammar of the fold subset |
+| [`evaluation.md`](./evaluation.md) | `F-Eval-*` | J1 expression evaluation |
+| [`verdict.md`](./verdict.md) | bare `F-*` | J2 the per-file verdict |
+| [`taint.md`](./taint.md) | bare `F-*` | J3 the identity-taint fixpoint |
+| [`observables.md`](./observables.md) | `F-Obs-*` | J4 properties and observables |
+| [`values.md`](./values.md) | `F-Val-*` | the value domain |
+| [`divergence.md`](./divergence.md) | `F-Direction`, `F-Div-*`, `F-Exc-*` | divergence between the shape classifier and the folder |
+| [`hosts.md`](./hosts.md) | `F-Host-*` | the host interface |
+| [`rules.md`](./rules.md) | `F-Rule-*` | rules over values |
+
+J1 through J4 are indexed in [`judgments.md`](./judgments.md).
+
+Nothing in the three appendices is normative. The reasoning that motivated
+each rule is in [`rationale.md`](./rationale.md).
+[`inventory.md`](./inventory.md) is the coverage ledger. Every decision
 point in chant core cites the rule that governs it and CI gates on it.
 [`prior-art.md`](./prior-art.md) surveys the neighboring systems and says
 where each one is nearest.
@@ -36,7 +38,7 @@ These govern the document set rather than the mechanism. CI structure enforces t
 
 - **Every normative rule carries a stable identifier**.
 - **Every identifier is exercised by at least one fixture and every fixture
-   cites a real identifier.** Both directions in CI.
+   cites a real identifier**. Both directions in CI.
 - **Rejections are located.** Node and rule. Message stability is not normative.
 - **The subset is versioned**. The policy is the Versioning section below; the current version is `VERSION` and the history is `CHANGELOG.md`.
 
@@ -99,21 +101,25 @@ The ordering above is a policy. What follows is the record of where it was
 exercised. It exists so that "extracted from chant" can be checked rather than
 assumed.
 
-**`S-ExportDefault`.** A default export is the declarator named `default`.
+### `S-ExportDefault`
+
+A default export is the declarator named `default`.
 The profile table admits it in `data-host`. In `full` it is permitted rather
 than required, and chant does not yet admit it. forgejo-warden's loader asks
 for that form. Its error message tells a user to export the policy as
 `export default`. It accepts `export const policy` as a fallback. That form
-folds as an ordinary `S-TopConst` export. So the form warden instructs its
-users to write is one chant cannot fold.
+folds as an ordinary `S-TopConst` export. That leaves chant unable to fold the form warden instructs its users
+to write.
+
+### `F-Profile-DataHost`
 
-**`F-Profile-DataHost`.** chant has no equivalent mode. The profile exists for
+chant has no equivalent mode. The profile exists for
 an evaluator with no JavaScript runtime. warden names it explicitly and folds
 with an empty host.
 
 Those two answer the transcription charge. A document transcribed from chant
-would carry neither. warden would still run because its fallback form folds
-without `S-ExportDefault`. The form it teaches would not fold and the profile
+would carry neither. With its fallback form folding without
+`S-ExportDefault`, warden would still run. The form it teaches would not fold and the profile
 it names would not exist.
 
 The rest are smaller and none has a consumer yet.
@@ -135,35 +141,35 @@ The rest are smaller and none has a consumer yet.
 and their normative text at a point in time recorded in
 [`VERSION`](./VERSION) as `major.minor` and tagged `spec-<major>.<minor>`
 on the commit that set it. It is not a chant release: chant declares which
-specification version it implements and the two move separately. It is not
-a revision of the rationale, the inventory, a note or a fixture, none of
-which is normative; a change confined to those does not move the version
+specification version it implements and the two move separately. A revision
+of the rationale, the inventory, a note or a fixture is not a version either,
+since none of those is normative; a change confined to those does not move the version
 and is not entered in [`CHANGELOG.md`](./CHANGELOG.md).
 
 **Four kinds of change.** A rule is *added* or
 *widened* when source that did not fold now does; the minor version moves,
 existing source is unaffected, and an implementation claiming the new
-version must implement the rule. A rule is *narrowed* when source that
-folded no longer does, or a verdict changes; the major version moves,
-because a project that folded under the old version may not under the new.
-A rule is *retired* when it is struck through in place with a note naming
-its successor (the identifier rules above); that is also major, and the
+version must implement the rule. When source that folded no longer does or
+a verdict changes, the rule is *narrowed*; the major version moves, because
+a project that folded under the old version may not under the new. Striking
+a rule through in place with a note naming its successor (the identifier
+rules above) *retires* it; that is also major, and the
 fixtures citing it move to the successor in the same change, which the
 coverage gate enforces, since a struck identifier is no longer defined and
 a citation of it fails.
 
 **A host obligation moves the minor.** The major exists for the reason
-*narrowed* gives. That reason is about a project's source. An obligation on
-the host is not about source at all. It constrains the implementation. Every
+*narrowed* gives. That reason is about a project's source, and an obligation
+on the host is not about source at all. It constrains the implementation. Every
 file that folded still folds under any host that still conforms. What narrows
 is the set of conforming hosts. That is the *added* case. Claiming the new
 version requires meeting the obligation. Implementing a new rule requires the
 same. Withdrawal is the reverse and is also minor.
 
-`F-Host-Interface` item 1 is the case that settled it. Bounding what an entity
-constructor may do at 2.1 stopped a validating host from conforming. No source
+The case that settled it is `F-Host-Interface` item 1. At `2.1`, bounding what
+an entity constructor may do stopped a validating host from conforming. No source
 changed verdict. The everyday reading of "a host that conformed no longer
-does" says major. The four kinds do not say it. 2.1 landed minor on the
+does" says major. The four kinds do not say it. `2.1` landed minor on the
 reading above and this paragraph is what records it (#204).
 
 **Two profiles.** `objective.md`
@@ -210,7 +216,7 @@ TypeScript as data.
 ### Fixed to TypeScript
 
 The syntax is the TypeScript AST as the `typescript`
-compiler package parses it; the module system is ES modules; and the semantics
+compiler package parses it and the module system is ES modules. The semantics
 of every admitted operator are ECMAScript's, stated per operator, because a
 second implementation in another language must reproduce ECMAScript coercion
 rather than its host's. Two places depart from
@@ -263,11 +269,12 @@ partial.
 
 Two families of identifier and the family is part of the meaning:
 
-- **`S-*`** is a *shape* rule decidable from syntax alone by a classifier
-  with no binding resolver and no registry. Lives in `grammar.md`. An `S-`
+- Shape rules, decidable from syntax alone by a classifier with no binding
+  resolver and no registry, carry `S-*`. They live in `grammar.md`. An `S-`
   rule may accept what an `F-` rule later rejects; never the reverse
   (`F-Direction`).
-- **`F-*`** is a *fold* rule. It cannot be decided from syntax alone. Its sub-prefix names the file that owns it.
+- Syntax alone cannot decide a *fold* rule and fold rules carry `F-*`. The
+  sub-prefix names the file that owns the rule.
 
 | Prefix | Owner |
 |---|---|
@@ -284,10 +291,10 @@ read alone, like `F-Eval-Member`. A rule with numbered steps is
 cited as `F-Eval-Member step 4`; the step number is not part of the
 identifier.
 
-**Stability.** An identifier names one rule for the life of the spec. A rule
+**Stability.** For the life of the spec, an identifier names one rule. A rule
 that is split keeps its identifier on the part closest to its original
-meaning and the new part gets a new one. A rule that is removed or renamed
-is struck through in place with a note naming its successor; the identifier
+meaning and the new part gets a new one. One that is removed or renamed is
+struck through in place with a note naming its successor; the identifier
 is never reused. Inventory row identifiers (`L3.10`) follow the same rule.
 
 **Enforcement.** `spec/coverage.test.ts` asserts every inventory row
@@ -295,6 +302,6 @@ cites a defined rule. The reverse, every defined rule has a conformance
 fixture, is the other. Together they make an identifier that nothing
 exercises, or a citation of nothing, a CI failure rather than a drift.
 
-One vocabulary. `S-*` and `F-*` are the only normative identifiers, each
+One vocabulary. The only normative identifiers are `S-*` and `F-*`, each
 rule's reasoning is a non-normative note under it, and `inventory.md` cites
 rules only.
diff --git a/spec/divergence.md b/spec/divergence.md
index a080879..4330cdb 100644
--- a/spec/divergence.md
+++ b/spec/divergence.md
@@ -31,12 +31,11 @@ predicate a downstream tool asks "will this fold?", a tool with no registry
 must get an answer that is safe to act on, which means erring toward "it may
 run" (`subset.ts` module doc, point 2c).
 
-**Discharge.** By construction, both consumers import one classifier
-(`subset.ts`), so they cannot disagree on node kinds, operators or key shapes;
+**Discharge.** By construction both consumers import one classifier
+(`subset.ts`) and so cannot disagree on node kinds, operators or key shapes;
 every remaining disagreement is a *resolution* the classifier does not
-perform, enumerated below. And by fixture, one accepting and one rejecting
-fixture per row of F-Div, asserting the classifier's and the folder's verdicts
-side by side. chant's `subset-doc-parity.test.ts` is the precedent.
+perform, enumerated below. One accepting and one rejecting fixture per row of
+F-Div assert the classifier's and the folder's verdicts side by side. chant's `subset-doc-parity.test.ts` is the precedent.
 
 ## F-Div (the divergences in the permitted direction)
 
@@ -63,7 +62,7 @@ one.
 
 ## F-Exc (the two exceptions)
 
-Shape rejects; the folder accepts. Each is stated with why it is tolerated
+Two constructs are rejected by shape and accepted by the folder. Each is stated with why it is tolerated
 rather than fixed.
 
 **F-Exc-Lazy.** Short-circuit laziness. The folder evaluates `&&`, `||`,
diff --git a/spec/grammar.md b/spec/grammar.md
index 0513446..567e187 100644
--- a/spec/grammar.md
+++ b/spec/grammar.md
@@ -1,9 +1,10 @@
 # Grammar of the fold subset
 
 Normative draft. Identifiers are `S-*`. Every production here is
-decidable from syntax alone. Where the folder is stricter than the shape rule,
-because it also resolves names or consults a registry, the production says
-so and names the `F-*` rule (evaluation.md, verdict.md) that adds the condition. That is
+decidable from syntax alone. The folder can be stricter than the shape rule
+because it also resolves names or consults a registry. Where it is, the
+production says so and names the `F-*` rule (evaluation.md, verdict.md) that
+adds the condition. That is
 the one direction F-Direction permits; a production must never be stricter
 than the folder.
 
@@ -12,9 +13,10 @@ Derived from `findSubsetViolation` (`subset.ts`), `fold()`
 `findFunctionSubsetViolation` and `findFactorySubsetViolation`, at
 `e4074c17`, with the `?.` forms from chant-v0.63.0 (`11572c7a`, #2328). Node kinds are TypeScript's.
 
-In the notation below, `⟨X⟩` is a nonterminal; `|` alternation; `*` zero or
-more; `+` one or more. Terminals are TypeScript tokens or node kinds. Each production cites
-its inventory row.
+In the notation below `⟨X⟩` is a nonterminal and `|` separates alternatives.
+Postfix `*` repeats an item any number of times including none and postfix
+`+` repeats it at least once. A terminal is a TypeScript token or a node
+kind. Each production cites its inventory row.
 
 ---
 
@@ -56,13 +58,13 @@ S-ExportTypeOnly    ::= export type { … }  |  a type-only element of S-ExportN
 
 Notes. Under S-ExportFunction an overload signature (no body) is skipped, not
 a disqualifier, and the bodied declaration that follows is the export.
-S-ReExport takes named elements only. Under S-ExportNamed a local name must be
-an identifier, and the TS 4.5 string module-export-name form disqualifies.
+S-ReExport takes named elements only. A local name under S-ExportNamed must be
+an identifier and the TS 4.5 string module-export-name form disqualifies.
 
 S-ExportDefault is the declarator named `default`, admitted in the
 `data-host` profile; in `full` it stays a disqualifier
 until chant admits it, which the profile table records as permitted and not
-required. `export default function` and `export =` disqualify in both.
+required. Both profiles disqualify `export default function` and `export =`.
 
 ```
 S-Disqualify ::= export default …                              -- full only; data-host admits S-ExportDefault
@@ -154,12 +156,23 @@ Only the bare-identifier part is decidable from syntax. The four conditions
 are resolution so S-CompositeStep admits any call at shape level and
 F-Eval-Member step 2 applies the full test.
 
-**Explicitly outside the subset** (S-Reject at shape level, and rejected by
-the folder): an arrow or function expression as a value (L3.1); class
-expressions; `await`, `yield`; assignment and compound assignment; the comma
-operator; `typeof`, `void`, `delete`, `++`, `--`; `==`, `!=`, `%`, `**`, the
-bitwise operators, `in`, `instanceof`; a computed property name; a
-non-literal element-access key; a call not matching any S-Call form. Optional chaining is
+The table below is what is explicitly outside the subset. S-Reject rejects
+each entry at shape level and the folder rejects it as well.
+
+| Explicitly outside the subset |
+|---|
+| an arrow or function expression as a value (L3.1) |
+| class expressions |
+| `await`, `yield` |
+| assignment and compound assignment |
+| the comma operator |
+| `typeof`, `void`, `delete`, `++`, `--` |
+| `==`, `!=`, `%`, `**`, the bitwise operators, `in`, `instanceof` |
+| a computed property name |
+| a non-literal element-access key |
+| a call not matching any S-Call form |
+
+Optional chaining is
 specified rather than merely admitted: since chant-v0.63.0 a `?.` on a nullish object
 produces a chain-short-circuit value that propagates through the remaining
 `.`/`[]`/`!`/`?.()` of the same chain and becomes `undefined` at its end
@@ -194,7 +207,7 @@ S-FactoryBody   ::= ⟨Expr⟩
                   | { ( const … = ⟨Expr⟩ )*  return ⟨Expr⟩ }      -- must end in return; empty body rejected
 ```
 
-Inside S-FactoryBody the expression grammar **gains** `new` in any value
+The expression grammar of S-FactoryBody **gains** `new` in any value
 position and a call through a bare identifier (a nested composite, a
 registered helper, an opted-in intrinsic), and a method call stays out (per
 the contract above `resolveInterpretableFactory`; `checkFactoryExpression`'s
@@ -208,7 +221,8 @@ inherits.
 
 ## What this grammar does not decide
 
-Resolution, registration, trust, the fold/run verdict and
-its taint (verdict.md, taint.md), and every semantic rule. A string that
+Outside it are resolution, registration and trust. The fold/run verdict and
+its taint (verdict.md, taint.md) are outside it as well and so is every
+semantic rule. A string that
 parses under this grammar is *shape-admissible*; whether it folds is the
 judgments' question.
diff --git a/spec/hosts.md b/spec/hosts.md
index e542230..c67365d 100644
--- a/spec/hosts.md
+++ b/spec/hosts.md
@@ -35,20 +35,20 @@ what the trust rules need, and the last is the rules contract's.
    reading one on a live instance yields an `AttrRef` bound to that instance
    (F-Val-Live) and on a *name* yields the `{__attrRef}` envelope.
 3. An intrinsic registry `ρ`: a list of `IntrinsicDef`.
-4. An authoring-helper allowlist: names a call may fold through as a
+4. An authoring-helper allowlist of the names a call may fold through as a
    `{__helper}` envelope.
-5. A trust set: the package specifiers this build resolved and loaded
+5. A trust set of the package specifiers this build resolved and loaded
    (arm 1) plus the host's own module tree (arm 2).
 6. A composite registration form, `export const N = Composite(fn, "N")`
    with `Composite` imported from the host, that makes a project-defined
    factory *interpretable*.
-7. Rules: the host's semantic checks over the folded namespace and the
-   artifact under the contract of `rules.md` (F-Rule-Supply). A project may
+7. Rules (the host's semantic checks over the folded namespace and the
+   artifact) under the contract of `rules.md` (F-Rule-Supply). A project may
    supply more as a policy.
 
 In the `data-host` profile (F-Profile-DataHost, objective.md) a host is a
-description rather than code: item 3, item 5, and a serialization mapping
-that says what each envelope becomes in the artifact. Items 1, 2, 4 and 6
+description rather than code. It consists of items 3 and 5 and a
+serialization mapping that says what each envelope becomes in the artifact. Items 1, 2, 4 and 6
 need something to invoke and are absent.
 
 ## F-Host-Registry (the shape of an intrinsic registration)
@@ -60,12 +60,12 @@ IntrinsicDef = { name, isTag: boolean, foldsAsCall?: boolean, foldsEagerly?: boo
 - `isTag` is **required**. An omitted value once defaulted silently to "not a
   tag" and shipped the most-used intrinsic in the ecosystem unfoldable. A
   registry entry that does not say which kind it is is invalid.
-- `isTag`, `foldsAsCall` and `foldsEagerly` are **mutually exclusive**. The
-  three fold predicates are: tag folds iff `isTag`; call form folds iff
-  `¬isTag ∧ foldsAsCall`; eager folds iff `¬isTag ∧ foldsEagerly`.
-- `foldsAsCall` and `foldsEagerly` are **opt-in, per intrinsic, default
-  off**, and never inferred from the name, the tag flag, or the call's shape
-  (closed allowlists).
+- `isTag`, `foldsAsCall` and `foldsEagerly` are **mutually exclusive**. There
+  are three fold predicates. A tag folds iff `isTag`. The call form folds iff
+  `¬isTag ∧ foldsAsCall` and the eager form iff `¬isTag ∧ foldsEagerly`.
+- The flags `foldsAsCall` and `foldsEagerly` are **opt-in per intrinsic and
+  default off**. Neither is ever inferred from the name or the tag flag or the
+  call's shape (closed allowlists).
 - A registration is **validated against the export it names**, tagged
   template signature versus plain call, and presence in the package's own
   exports (`chant dev check-lexicon`). A host must provide the equivalent
@@ -78,7 +78,8 @@ A call-form intrinsic, an eager intrinsic, or an authoring helper qualifies
 
 - it is a **pure function of its arguments**, no I/O, no environment read,
   no module-level mutable state, no observable side effect;
-- it builds a **deterministic envelope or plain data** from them;
+- the output it builds from them is a **deterministic envelope or plain
+  data**;
 - **invoking it at fold time is indistinguishable from invoking it during a
   real run** of the file.
 
@@ -86,15 +87,15 @@ That third clause is the whole correctness argument for every registered
 call, and it is the same-function principle: revival invokes the function the
 file's `import` names, never a reimplementation (F-Host-NoSubstitution).
 
-Explicitly excluded by chant, with the reason each fails:
+Explicitly excluded by chant with the reason each fails:
 
-- `env()`, which reads `process.env`.
-- `Op()`, which returns an entity. An entity-returning factory is the
+- `env()` reads `process.env`.
+- `Op()` returns an entity. An entity-returning factory is the
   nested-construction hazard wearing a call.
-- `propagate()`, `withDefaults()`, `resource()`, `mergeDefaults()`, which are
+- `propagate()`, `withDefaults()`, `resource()` and `mergeDefaults()` are
   composite *definition* helpers, and `propagate` mutates in place.
-- `createResource()` and `createProperty()`, which build classes at a module's
-  top level, never as a value.
+- Both `createResource()` and `createProperty()` build classes at a module's
+  top level and never as a value.
 
 ## F-Host-Closed-vs-Open (why packages are closed and project files are open)
 
@@ -105,7 +106,7 @@ A call into a **package** folds only two ways:
 - At a declarator, by invocation (F-Call), reached directly or through a const
   alias (F-Declarator), where the result is a value whatever it is.
 
-A call written inside an expression never folds through a package. Its
+Nothing folds through a package from a call written inside an expression. Its
 *result* may be read in one place. Inside an argument of a call F-Call
 resolves, a reference to a top-level `const` bound to a package call reads
 the instance F-Call made for it (F-Call, *Reads in an argument*). The call
@@ -116,10 +117,10 @@ with no allowlist.
 The asymmetry is the trust boundary. Package code is already
 loaded and executed by the build before discovery begins; admitting a call
 into it costs no execution the process was not performing so it is admitted
-by declaration and verified by registration. Project code is the untrusted
-input; it is admitted only when it can be *evaluated without being
-executed*, folded or interpreted, which a syntactic body check decides and
-an allowlist could not.
+by declaration and verified by registration. The untrusted input is project
+code. It is admitted only when it can be *evaluated without being executed*
+(folded or interpreted) and a syntactic body check decides that where an
+allowlist could not.
 
 ## F-Host-NoSubstitution (the function that runs is the one imported)
 
@@ -165,7 +166,8 @@ Two arms, and nothing else:
 
 1. A specifier that is an active package of this build, or a subpath of one,
    matched by text against the closed set the build already resolved.
-2. A specifier that *resolves* to a path inside the host's own module tree.
+2. Any import whose specifier *resolves* to a path inside the host's own
+   module tree.
    Text is insufficient here because an untrusted repository controls both
    its source and its `node_modules`.
 
@@ -174,10 +176,19 @@ outside both arms is F-IsolatedRefusal (J2).
 
 ## F-Host-Generality (what varies and what does not)
 
-A host may vary the seven items of F-Host-Interface. It may not vary
-the syntax (grammar.md), the semantics of admitted operators (J1), the
-module system, the value domain's shape (values.md), the judgments (J1–J3),
-and the direction claim (divergence.md). Generality is over **host
+The seven items of F-Host-Interface may vary from host to host. Nothing in
+this table may.
+
+| Fixed for every host | Where |
+|---|---|
+| the syntax | grammar.md |
+| the semantics of admitted operators | J1 |
+| the module system | |
+| the value domain's shape | values.md |
+| the judgments | J1–J3 |
+| the direction claim | divergence.md |
+
+Generality is over **host
 vocabularies** (`README.md`, Scope). A host is one
 instantiation; chant's lexicons are the reference instantiation and the
 reference implementation is meant to carry the interface without
diff --git a/spec/inventory.md b/spec/inventory.md
index 6d4eb49..3228c2e 100644
--- a/spec/inventory.md
+++ b/spec/inventory.md
@@ -3,10 +3,10 @@
 Every decision point in chant core's fold path with the requirement that covers
 it. Derived from a complete read of the four files below.
 
-A **decision point** is anywhere the mechanism chooses between admitting and
-rejecting, between evaluation modes, or between representations. One row each.
-Rows are not lines of code; several rows can live in one function and one row
-can span several.
+A **decision point** is anywhere the mechanism admits or rejects or chooses
+an evaluation mode or a representation. Each gets one row. A row
+is not a line of code; several rows can live in one function and one row can
+span several.
 
 | File | Read |
 |---|---|
@@ -224,8 +224,8 @@ module is never imported.
 
 **The rule for the column.** A row is *covered* only when a specific rule
 (`S-Template`, `F-Eval-Member step 4`, `F-Val-Fate`) governs what the row
-does. A citation of a whole file or judgment is not coverage. A partially
-covered row is GAP. There is no double counting, and the coverage gate checks
+does. A citation of a whole file or judgment is not coverage. Partial
+coverage is GAP. There is no double counting, and the coverage gate checks
 that every cited identifier is defined in a spec file.
 
 | | Rows | Covered | GAP |
@@ -244,7 +244,7 @@ that every cited identifier is defined in a spec file.
 | L12 generators | 4 | 4 | 0 |
 | **total** | **128** | **128** | **0** |
 
-**Row identifiers are stable and append-only.** `L3.10` names one decision
+The numbering is stable and append-only. `L3.10` names one decision
 point forever; a new row in a layer takes the next number and nothing is ever
 renumbered. A row that turns out to be wrong is struck through with a note, not
 removed, so a citation of it stays resolvable. Row identifiers are as stable as rule identifiers and for the same reason:
diff --git a/spec/judgments.md b/spec/judgments.md
index 1ffc10f..8b30c90 100644
--- a/spec/judgments.md
+++ b/spec/judgments.md
@@ -8,7 +8,7 @@ decidable from syntax.
 The objective all three serve, the two profiles, and the notation they are
 written in are [`objective.md`](./objective.md).
 
-- [`evaluation.md`](./evaluation.md), J1, expression evaluation `Γ, H ⊢ e ⇓ v`.
-- [`verdict.md`](./verdict.md), J2, the per-file verdict `B, ι ⊢ f ⇓ fold(X, L) | run(reason)`.
-- [`taint.md`](./taint.md), J3, the identity-taint fixpoint.
-- [`observables.md`](./observables.md), J4, properties and observables.
+- J1, expression evaluation `Γ, H ⊢ e ⇓ v`, is [`evaluation.md`](./evaluation.md).
+- J2, the per-file verdict `B, ι ⊢ f ⇓ fold(X, L) | run(reason)`, is [`verdict.md`](./verdict.md).
+- J3, the identity-taint fixpoint, is [`taint.md`](./taint.md).
+- J4, properties and observables, is [`observables.md`](./observables.md).
diff --git a/spec/prior-art.md b/spec/prior-art.md
index ac30b97..ceff841 100644
--- a/spec/prior-art.md
+++ b/spec/prior-art.md
@@ -42,7 +42,7 @@ it evaluates global code. Next.js prerenders a page by rendering it.
 
 Constant folding is the exception and it is the shallow end. A compiler
 reducing `2 + 3` runs no function of the user's. The technique is
-expression-local. It preserves semantics and a compiler may skip it entirely.
+expression-local. Semantics are preserved and a compiler may skip it entirely.
 Nobody builds a configuration mechanism on it because on its own it reaches
 nothing.
 
@@ -81,11 +81,11 @@ CTFE decides per *call site*. The specification (dlang/dmd,
 `spec/function.dd`, "Compile Time Function Execution") lists the contexts
 "where a compile time value is required" and states the principle this work
 relies on: "All functions that execute in CTFE must also be executable at run
-time. The compile time evaluation of a function does the equivalent of running
-the function at run time. The semantics of a function cannot depend on compile
-time values of the function."
+time." It adds that compile time evaluation "does the equivalent of running
+the function at run time" and that "the semantics of a function cannot depend
+on compile time values of the function".
 
-CTFE obtains the value by running the function. The quoted sentence says so
+Running the function is how CTFE obtains the value. The quoted sentence says so
 and it is the difference this work turns on rather than a detail of it.
 
 A required context that cannot be evaluated is illegal and there is no
@@ -96,7 +96,7 @@ operations which are forbidden in CTFE". chant decides per *file* and a file
 that cannot be folded is run.
 
 A CTFE'd value is *copied* into the compiled program so nothing at run time
-shares identity with a compile-time object. chant's folded entities are the
+shares identity with a compile-time object. The entities chant folds are the
 same objects the run path would have built and other files hold references to
 them. That is the whole reason the taint fixpoint exists and CTFE has no
 analogue because it has no such sharing.
@@ -114,9 +114,8 @@ at build time and per-request rendering runs it later.
 
 There, the decision is by a *syntactic marker the author
 writes*, and an analysis of whether the unit is statically evaluable plays no
-part; and
-statically-rendered and server-rendered pages share no runtime object identity
-across the boundary, so there is nothing to taint. The equivalence obligation
+part. Since statically-rendered and server-rendered pages share no runtime
+object identity across the boundary, nothing is left to taint either. The equivalence obligation
 is also never stated as a discharged property.
 
 ### Partial evaluation of JavaScript (Prepack)
@@ -132,7 +131,7 @@ and keeps identity trivially because the residual program is one program with
 one heap. chant's choice of a coarse per-file decision is what makes identity
 non-trivial. Prepack's own limitation is instructive for the paper: it has no
 model of `document` or `window` and such reads "evaluate to `undefined`".
-That is the silent-undefined hazard INTENTIUS/chant#2328 records in `fold()`'s
+INTENTIUS/chant#2328 records the same silent-undefined hazard in `fold()`'s
 property-access branch.
 
 On the identity question specifically: Prepack's `ResidualHeapVisitor`
@@ -208,9 +207,9 @@ from a code file such as `tsconfig.ts` or `tsconfig.d.ts` and take the type of
 its `default` export as the configuration object. Imports and spreads compose
 a configuration and the file is never executed. The description gives the
 reason in the author's words: they "really did just want the syntactic
-niceties like imports and spreads". The PR was closed unmerged on 2024-05-21. It had no tests or
-diagnostics or language-service support. The thread records no reason for
-closing.
+niceties like imports and spreads". The PR was closed unmerged on 2024-05-21, with no tests or
+diagnostics or language-service support, and no reason for closing is
+recorded.
 
 The thread is short. It opened on 1 April and drew seven comments. The
 TypeScript bot left three and the author one. Readers left the other three.
@@ -255,8 +254,8 @@ that into `tsconfig.json`. The PR itself points at that discussion
 (microsoft/TypeScript#57486).
 
 This work sits in that valley on purpose. The edge of the subset is specified
-(grammar.md). Source past the edge falls back to running and the two paths
-must agree (objective.md). The semantics are versioned with the specification
+(`grammar.md`). Source past the edge falls back to running and the two paths
+must agree (`objective.md`). The semantics are versioned with the specification
 (`spec/VERSION`). A change in the checker's widening or contextual typing
 cannot move a folded value. Reading a configuration off checker inference
 inherits every such change.
@@ -295,7 +294,7 @@ resumes with the contents. The community's own framing is that
 IFD "is bind" for Nix builds. It is an escape from pure evaluation that keeps
 the result deterministic because the build is sandboxed and content-addressed.
 
-IFD escapes into a *build* of something else; chant's
+What it escapes into is a *build* of something else; chant's
 fallback executes *the source file itself*. IFD is the better precedent for
 `--sandbox` than for folding and belongs in the isolation discussion.
 
@@ -378,8 +377,8 @@ explicit in the language rather than inferred.
 2. Same-function agreement via revival through the file's own imports.
    Precedented by CTFE's design principle and citable as the same argument.
 3. Byte-identical agreement as a discharged obligation over a real corpus.
-   Not found in this sweep as a stated, tested property, and not searched for
-   specifically. A methodological contribution.
+   This sweep did not find it as a stated and tested property nor search
+   for it specifically. A methodological contribution.
 4. Bidirectional identity taint over the module graph so that a shared entity
    is never two objects when one side folds and the other runs. No precedent
    found. It follows from per-file granularity with shared identity. No
diff --git a/spec/rationale.md b/spec/rationale.md
index 620a131..27ff0cd 100644
--- a/spec/rationale.md
+++ b/spec/rationale.md
@@ -30,12 +30,27 @@ admissibility rules and an implementer will conflate them.
 
 **S-Module, S-Disqualify** *(Admissibility is decided at two layers: the statement gate runs first and disqualifies whole files)*
 
-`scanExports` (L1.1–L1.6) recognizes exactly: `export const X = new Type(...)`,
-`export const X = <expr>`, `export const {a, b} = <expr>`, `export {a, b}`,
-`export {a, b} from "./m"`, and `export function f() {}`. Anything else
-disqualifies the file: `export default`, `export * from`, an exported class,
-`let`/`var`, a destructured export with a rest, nested or defaulted element.
-`export type {...}` and type-only re-export elements are erased (L1.6).
+`scanExports` (L1.1–L1.6) recognizes exactly the forms in the first table.
+Anything else disqualifies the file. The second table has examples.
+
+| Recognized |
+|---|
+| `export const X = new Type(...)` |
+| `export const X = <expr>` |
+| `export const {a, b} = <expr>` |
+| `export {a, b}` |
+| `export {a, b} from "./m"` |
+| `export function f() {}` |
+
+| Disqualifying |
+|---|
+| `export default` |
+| `export * from` |
+| an exported class |
+| `let`/`var` |
+| a destructured export with a rest, nested or defaulted element |
+
+Both `export type {...}` and type-only re-export elements are erased (L1.6).
 
 **§2** *(The expression layer)*
 
@@ -73,7 +88,7 @@ resource is a live instance in `full` and an envelope in `data-host`
 one would make its answer depend on which profile ran. That is the thing
 `F-Host-Generality` exists to prevent.
 
-Two more are decided on their own terms. `==` and `!=` coerce. A subset whose
+Two more are decided on their own terms. The operators `==` and `!=` coerce. A subset whose
 point is that a value is fixed by its source should not carry an operator
 whose answer turns on a conversion the reader has to know. `delete`, `++` and
 `--` mutate, and nothing in the subset has a place to put the effect.
@@ -106,9 +121,8 @@ own statements (`fold-import.ts` module doc).
 
 **F-IsolatedRefusal** *(Isolation changes what folds so it is part of the mechanism)*
 
-Under sandboxed execution a fold whose revival would invoke *project-owned*
-code is refused and the file falls back to run (L9.5,
-INTENTIUS/chant#1093). The fold/run decision is therefore parameterized by
+Sandboxed execution refuses a fold whose revival would invoke *project-owned*
+code and the file falls back to run (L9.5, INTENTIUS/chant#1093). The fold/run decision is therefore parameterized by
 whether project code may execute in this process.
 
 Isolation is an optional capability, modelled in the
@@ -118,8 +132,8 @@ is `run`, not `fold` (F-IsolatedRefusal, judgments.md). `executing` is the
 opposite opt-in, under which a declared project function whose body
 cannot fold is invoked at a declarator (F-Call step 2), so the fold may
 depend on the folding process. It is never the default since a fold that reads the
-environment silently is what chant#2453 found. An implementation declares
-which modes it supports; conformance reports them separately and requires
+environment silently is what chant#2453 found. Which modes are supported is
+declared by each implementation; conformance reports them separately and requires
 neither `isolated` nor `executing`. The observable is `projectFactoryInvocations`
 counter which must be zero for every folded file under `isolated`. Nix
 import-from-derivation is the cited precedent for evaluation escaping into a
@@ -141,8 +155,8 @@ requirement is checked rather than trusted.
 Two entry points exist. `tryFoldFile` returns a `FoldFileResult` (L8.1)
 either ok with the complete export namespace or a reason. One unrecognized export disqualifies the file (L8.2). `foldModule`
 (L8.3) is per-export, carries an ok/false entry per declaration, and silently
-skips non-`new` exports. **The per-file entry point is normative**; the
-per-export one is a diagnostic surface.
+skips non-`new` exports. **The per-file entry point is normative**;
+`foldModule` is a diagnostic surface.
 
 The reason fallback is per-module rather than per-declaration is stated in the
 statement gate itself (L1.7) and belongs in the spec: an unfoldable export can
@@ -152,16 +166,16 @@ reference or be referenced by a foldable one in ways only running proves safe.
 
 `planFoldTaint` (L8.6–L8.8):
 
-- **Forward along imports.** A tainted file taints every file it imports or
+- **Forward along imports**. A tainted file taints every file it imports or
   re-exports from: if `f` runs, its real import of `g` constructs `g`'s
   entities, and a folded `g` would be a second copy, so `g` runs even if it
   would have folded alone. Reading it the other way round, as an importer of a
   non-folding file being tainted, describes J2's resolution failure putting
   the importer in the seed. That happens earlier than this walk.
-- **Reverse.** A file whose *objects were captured* by an already-folded file
+- **Reverse**. A file whose *objects were captured* by an already-folded file
   taints the capturer. `liveSources` records only non-primitive captures
   (L8.5) because a primitive has no identity to disagree about.
-- **Through calls.** A project-local function whose call *returns* a live
+- **Through calls**. A project-local function whose call *returns* a live
   object the body produced (not one merely passed through the arguments)
   records the same taint edge (L5.9, `leakedIdentity`). Identity propagates
   through invocation as well as through import.
@@ -232,8 +246,8 @@ relationship folds while the other runs.
 **F-Eval-New, F-Eval-Tagged, F-Eval-CallHelper, F-Eval-CallIntrinsic, F-Eval-Member step 2** *(Admissibility depends on where the expression sits)*
 
 Five constructs that fold at a file's top level are refused inside a folded
-function body: `new`, a tagged template, a helper call, an intrinsic call, and
-`.step` (L3.16, `functionBodyDepth`). Each produces an envelope revived against
+function body (L3.16, `functionBodyDepth`). They are `new` and `.step`, a
+tagged template, and a helper or intrinsic call. Each produces an envelope revived against
 the *caller's* imports which is not the scope the body was written in.
 `new ns.Type(...)` is refused everywhere because a namespace-qualified
 constructor cannot be resolved through named imports (L3.15).
@@ -248,7 +262,7 @@ const of the same name.
 **F-Bind, F-Eval-Ident, F-Eval-CallLocal** *(What a binding is and the order names resolve in)*
 
 **A top-level binding is a `const` with an identifier name and an initializer**
-(`collectConsts`, L5.1). A top-level destructured `const`
+(`collectConsts`, L5.1). A destructured `const` at top level
 (`const { a } = …`) does not bind `a` for the folder and a non-exported
 `const` is collected exactly like an exported one. The spec must say this
 because the first is a surprise. The declaration is valid TypeScript and the
@@ -256,12 +270,12 @@ name is invisible.
 
 **Lookup order is `consts`, then `externals`** (L5.2, `fold.ts` identifier
 branch). A name in the file's own `consts` is never looked up in `externals`.
-The order is the rule and shadowing is its consequence.
+Shadowing follows from the order and the order is the rule.
 
 **A project-local function's body folds in the defining module's scope**
 (L5.5, `callFoldableFunction`): the arguments fold in the caller's `consts`/
-`externals`; the body folds against a copy of the *callee's* `consts` and
-`externals`, with each parameter bound by deleting the name from that copy of
+`externals`; a copy of the *callee's* `consts` and `externals` is what the
+body folds against, with each parameter bound by deleting the name from that copy of
 `consts` and setting it in `externals` (so a parameter shadows a module-level
 const of the same name); `externals` are read live, so a function declared
 before a const it reads still sees the const's value. states the same
@@ -304,9 +318,9 @@ ordinary use coerces the result to string during folding, before any revival
 would run.
 
 A method call on a real receiver (L2.14) is the same mode. The receiver is the
-same object either way so calling it is what running would do. Both are
-places where fold time and revival time are observably different and the spec
-must name them as such.
+same object either way so calling it is what running would do. In both, fold
+time and revival time are observably different, and the spec must name them
+as such.
 
 ---
 
@@ -333,7 +347,7 @@ states.
 
 `setPathProvenance` (L10.2) records, during fold, which composite parameter
 produced which emitted field; the first (innermost) writer wins. It is real
-output and it is useful. It is **not** part of the objective: the run path
+output and useful but **not** part of the objective: the run path
 obtains provenance, where it has any, by a different mechanism, and making
 provenance normative would oblige fold and run to agree on a thing the run path
 does not uniformly produce.
@@ -352,16 +366,16 @@ invocations under isolation.
 
 **F-Obs-Report, F-Reason** *(Fallback reporting is normative)*
 
-A fallback must be reported. An unreported fallback is indistinguishable
+A fallback must be reported since an unreported one is indistinguishable
 from a fold and the guarantee becomes unauditable. A conforming implementation must report, per file, the
 decision taken and, for a fallback, a located reason (L10.3). The reason's
 wording is unconstrained.
 
 **Which location when there are two.** A rejection inside a project-local
 function body has a position in the callee's file and a call site in the
-caller's. The implementation re-throws at the **call site**, naming the callee and its
-file, the position inside it, and the reason, preserving the rule
-identifier (L5.10, `callFoldableFunction`). The reported location is the call;
+caller's. `callFoldableFunction` re-throws at the **call site** and preserves the rule
+identifier (L5.10). Its message names the callee with
+its file plus the position inside it and the reason. The reported location is the call;
 the callee position travels in the message. The spec must say which is
 primary because R-spec.3's "located" is otherwise ambiguous for exactly this
 case. Whether the report is summarized or verbose by default is a
@@ -387,8 +401,8 @@ wrong by assuming it.
 **F-Eval-Unary, F-Eval-Binary** *(Operators are ECMAScript's on the folded operand values)*
 
 The supported binary operators (L2.8, L3.14) are `+` `-` `*` `/` `===` `!==`
-`>` `<` `>=` `<=` and the lazy `&&` `||` `??` (L3.13). Unary `!` and `-`
-(L3.12). Conditional `?:`.
+`>` `<` `>=` `<=` and the lazy `&&` `||` `??` (L3.13). Unary `!` and `-` are
+supported too (L3.12) and so is the conditional `?:`.
 
 For every one of these the implementation applies the host JavaScript operator
 to the folded values, so the semantics are ECMAScript's: `+`'s
@@ -419,26 +433,26 @@ is the permitted direction, and the divergence list carries it.
 
 Property or element access on an identifier bound to a same-file `new` yields
 `{__attrRef: {entity, attribute}}` keyed by the identifier (L3.9). Access on a
-value that folded to a `{__resource}` envelope yields the same, but only when
-the object expression is a plain identifier, any other shape is refused,
+value that folded to a `{__resource}` envelope yields the same only when
+the object expression is a plain identifier. Any other shape is refused
 because there is no name to key the reference on and silently indexing the
 envelope produced wrong output (L3.11, chant#1535).
 
 **F-Eval-Template** *(Template spans coerce by ECMAScript `ToString`)*
 
-`String(fold(span))` (L3.2). For scalars that is ECMAScript. For a symbolic
+`String(fold(span))` (L3.2). On scalars this matches ECMAScript. For a symbolic
 envelope it is `"[object Object]"`, and the run path produces the same,
 because `AttrRef` defines no `toString`.
 
-So fold and run agree and the output is silently wrong on both. That is why
+Fold and run therefore agree and the output is silently wrong on both. That is why
 `F-Div-TemplateEnvelope` refuses an envelope in a plain template span instead
 of inheriting `ToString` (L3.23).
 
 **F-Eval-Object, F-Eval-Array** *(Key and element ordering are ECMAScript's and byte-identity depends on it)*
 
-Object literals evaluate members in source order; spread is `Object.assign`
-so spread keys land in the source's insertion order and a later key wins
-(L3.3). Arrays preserve element order; spread splices in place. This is
+Object literals evaluate members in source order. Their spread is
+`Object.assign` so its keys land in the source's insertion order and a later
+key wins (L3.3). Arrays preserve element order and splice a spread in place. This is
 ECMAScript object-literal evaluation and "as ECMAScript" is available here.
 
 Whether order is *observable* depends on the emitter.
@@ -458,8 +472,8 @@ which hosts those are.
 
 **F-Eval-Object, F-Eval-Array** *(Spread departs from ECMAScript in one direction)*
 
-Object spread requires a non-null object; array spread requires
-`Array.isArray` (L3.4, L3.5). ECMAScript array spread accepts any iterable.
+Object spread requires a non-null object and an array spread here requires
+`Array.isArray` (L3.4, L3.5) where ECMAScript accepts any iterable.
 `[...'ab']` is `['a','b']` there and a rejection here. A deliberate narrowing
 and one a second implementation would not infer from "as ECMAScript".
 
@@ -471,7 +485,7 @@ and one a second implementation would not infer from "as ECMAScript".
 
 The spec must define what a fold produces. Every other requirement quantifies
 over it and it is currently defined only by a TypeScript union
-(`FoldedValue`, `fold.ts`; L4.1).
+(`FoldedValue` in `fold.ts`, L4.1).
 
 The scalars with `undefined` beside them, plus arrays and plain objects, are
 ordinary JSON. The rest carry envelopes.
@@ -577,9 +591,9 @@ build-parameters documentation true ("dropped from the output in both JSON and
 YAML rather than shipped as `null`").
 
 The two facts are the difference between "absent" and "null" which platforms
-treat differently. For the six YAML-native
-lexicons above, the walker's `undefined` reaches *their* emitter directly, so
-the rule there is each serializer's and not `JSON.stringify`'s.
+treat differently. In the six YAML-native lexicons above the walker's
+`undefined` reaches *their* emitter directly. The rule there is each
+serializer's own rather than `JSON.stringify`'s.
 
 **F-Val-Arity** *(Constructor arity)*
 
@@ -651,7 +665,7 @@ state.
 
 **What it does not catch.** A network call that answers the same twice. A
 read of an environment name the probe does not set. A constructor that is
-heavy but deterministic. Item 1 answers that one at 2.1.
+heavy but deterministic. Item 1 has answered that one since spec `2.1`.
 
 Partial in the way F-Obs-Counters is partial and shipped for the same
 reason. A check that catches the cheap cases beats an obligation nothing
@@ -665,7 +679,7 @@ those would measure the harness.
 **F-Host-Interface item 1** *(What a constructor may do)*
 
 Item 1 enumerated what an entity carries and said nothing about what building
-one may do. Revival invokes that constructor (F-Val-Fate). Item 1 was the
+one may do. Since revival invokes that constructor (F-Val-Fate), item 1 was the
 one place code runs during a fold with no bound on it. An intrinsic has
 F-Host-Admission and a rule has F-Rule-Pure. A constructor had only the shape
 of its output and a host could build a dependency graph behind one and
@@ -684,7 +698,7 @@ author at the keystroke.
 
 The published measurement is a separate question. `paper/measurements.md`'s
 0 MB row records what a CPU profile could see and carries that instrument's
-floor. What 2.1 requires is the thinness that row reflects rather than the row
+floor. What `2.1` requires is the thinness that row reflects rather than the row
 itself. A constructor still runs under revival and counting one exactly is
 F-Obs-Counters' job.
 
diff --git a/spec/rules.md b/spec/rules.md
index 560957b..f9e6c9e 100644
--- a/spec/rules.md
+++ b/spec/rules.md
@@ -11,9 +11,9 @@ of every file in the build before anything is emitted and without running any
 of them so it runs wherever the fold runs and gives the answer a run would
 have given.
 
-Derived from chant's post-synthesis engine (`packages/core/src/lint/post-synth.ts`),
-its policy layer (`lint/policy.ts`), and its severity configuration
-(`lint/config.ts`), at `chant-v0.71.0`. chant's declarative `rule({…})`
+Derived from chant's post-synthesis engine
+(`packages/core/src/lint/post-synth.ts`) at `chant-v0.71.0` with the policy
+layer in `lint/policy.ts` and the severity configuration in `lint/config.ts`. chant's declarative `rule({…})`
 format matches AST nodes and is the classifier's territory (grammar.md);
 it is not a rule over values and is not covered here.
 
diff --git a/spec/taint.md b/spec/taint.md
index c480519..97df325 100644
--- a/spec/taint.md
+++ b/spec/taint.md
@@ -7,11 +7,11 @@ Derived from `planFoldTaint` (`fold-import.ts`),
 ### Why this judgment exists
 
 Per-file partial evaluation is unsound in the presence of object identity
-unless something makes it sound. If file `A` folds and file `B` runs, and both
-refer to an entity `e` that `A` produced, then `B`'s real import of `A`
-constructs a second `e`, and the build holds two objects for one entity,
-whose `AttrRef`s cannot both receive a logical name and whose `Ref`s silently
-inline instead of referencing.
+unless something makes it sound. Suppose file `A` folds while file `B` runs and
+both refer to an entity `e` that `A` produced. The real import of `A` by `B` then
+constructs a second `e`. The build holds two objects for one entity.
+That entity's `AttrRef`s cannot both receive a logical name and its `Ref`s
+silently inline instead of referencing.
 
 Every comparable system avoids the problem by not having it
 ([`prior-art.md`](./prior-art.md)). Compile-time function execution copies
@@ -42,8 +42,8 @@ are not interchangeable.
 - The **reference test** (F-Import) is `typeof` object **or** function. It does
   not recurse and it admits a plain `{ a: 1 }` that the entity test rejects.
 
-The proposition below is about *entities* — the values a build names and
-serializes — and the entity test is the normative one for it. Two structurally
+The proposition below is about *entities* (the values a build names and
+serializes) and the entity test is the normative one for it. Two structurally
 equal plain objects that no `AttrRef` points at cannot be told apart in the
 output so
 duplicating one breaks nothing claimed here. Recursion is what makes that test
@@ -130,8 +130,8 @@ The fixpoint itself is indifferent to cycles in `→`.
 
 **Proposition (one instance per entity).** In a build whose verdicts are
 `F-Verdict`, every entity `e` produced by the build is represented by exactly
-one object, and every reference to `e`, from a folded file's `X`, from a run
-file's import, from an `AttrRef`, is that object.
+one object. A reference to `e` in a folded file's `X` or a run file's import
+or an `AttrRef` is that object.
 
 **Lemma (capture implies import).** `f ⇝ g` implies `f → g`. F-Capture
 requires the captured value be reached through `f`'s resolved imports of `g`.
@@ -142,9 +142,9 @@ and `f` importing that binding from `h` records `f ⇝ h` alongside `f → h`.
 The closure composes the two.
 
 The fixpoint and this proposition are checked over every build of four files
-by `spec/taint-model.test.ts` (#179). That is 8,503,056 builds: every import
-relation excluding self-imports, every capture relation inside it, and every
-assignment of tentative verdicts. The scope is stated for the same reason
+by `spec/taint-model.test.ts` (#179). That is 8,503,056 builds, one per
+combination of import relation excluding self-imports, capture relation
+inside it and assignment of tentative verdicts. The scope is stated for the same reason
 F-Depth's bounds are. The check carries its own vacuity guards. One of them is
 the instance case 2 of the sketch below originally got wrong.
 
@@ -154,13 +154,13 @@ to `e`.
 1. If `g ∉ T(B)` then `g` folded and `e` is the object in `X(g)`, unique by
    F-Memo and F-Count. Suppose `f` folded. It obtained `e` through its
    resolved imports of `g` and therefore `f ⇝ g`. Were `f ∈ T(B)` the lemma
-   would give `f → g` and the forward edge would put `g ∈ T(B)`. So
-   `f ∉ T(B)` and its reference is the F-Memo object. Suppose instead `f`
-   runs. Then `f ∈ T(B)` and `f → g`, and the forward edge puts `g ∈ T(B)`
+   would give `f → g` and the forward edge would put `g ∈ T(B)`.
+   Hence `f ∉ T(B)` and its reference is the F-Memo object.
+   If `f` runs instead, then `f ∈ T(B)` and `f → g`, and the forward edge puts `g ∈ T(B)`
    again. Every referrer therefore folded and holds the one object.
 2. If `g ∈ T(B)` then `g` runs and `e` is constructed by real execution. `f`
    holds `e` through a binding imported from `g` or from a file that
-   re-exports it. Let `g'` be the first file on that chain whose verdict is
+   re-exports it. Let `g'` be the first file on that chain to have the verdict
    `run`. That is `g` itself for a direct import and is reached by the
    backward edge otherwise. J2 resolves a binding from `g'` only where `g'`
    folds. F-Import leaves it unresolved and records `g'`'s reason against it.
@@ -216,19 +216,18 @@ The evidence has two sources.
   The entry's own test asserts which file folds and which runs and the
   differential holds fold-versus-run across it.
 
-Four of the nine exercise this judgment on purpose, in one build:
+Four of the nine exercise this judgment on purpose in one build.
 
-- `taint-run-only-importer.ts`, F-Seed. An early `return` in a project-local
-  function puts the importer in the seed.
-- `taint-shared-config.ts`, F-Succ forward. The running importer pulls a
-  foldable config back.
-- `taint-capturing-sibling.ts`, F-Succ backward. The source of a captured
-  object pulls the capturer back.
-- `taint-independent.ts`, F-Taint/F-Fix. The control that no edge reaches and
-  that must still fold.
+| File | Rule | What it exercises |
+|---|---|---|
+| `taint-run-only-importer.ts` | F-Seed | An early `return` in a project-local function puts the importer in the seed. |
+| `taint-shared-config.ts` | F-Succ forward | The running importer pulls a foldable config back. |
+| `taint-capturing-sibling.ts` | F-Succ backward | The source of a captured object pulls the capturer back. |
+| `taint-independent.ts` | F-Taint/F-Fix | The control that no edge reaches and that must still fold. |
 
-The other five cover the `?.` short-circuit under F-Div-Nullish, plus
-F-Eval-Ident shadowing, F-Div-SpreadType and F-Depth.
+Among the other five are files for the `?.` short-circuit under
+F-Div-Nullish and for F-Eval-Ident shadowing; the rest cover F-Div-SpreadType
+and F-Depth.
 
 The incidental mixed entries and the one designed to fire both taint
 directions all agree. The corpus is still chant's own and the adversarial entry is one
diff --git a/spec/values.md b/spec/values.md
index 2e1a2c3..bd4ec83 100644
--- a/spec/values.md
+++ b/spec/values.md
@@ -31,9 +31,9 @@ live instance is a `v`, a live instance is what an envelope becomes
 
 ## F-Val-Envelope (six envelopes recognized by key)
 
-A value is an *envelope* iff it is a non-array object carrying one of the keys
-`__attrRef`, `__intrinsic`, `__helper`, `__resource`, `__compositeStep`,
-`__symbol` (`isFoldSymbolicEnvelope`). An envelope is a finished value that
+Any non-array object carrying one of the keys `__attrRef`, `__intrinsic`,
+`__helper`, `__resource`, `__compositeStep`, `__symbol`
+(`isFoldSymbolicEnvelope`) is an *envelope*, and no other value is. Each one is a finished value that
 *denotes* something not yet constructed; it is never a thunk and an
 implementation must not attempt to force it.
 
@@ -51,9 +51,10 @@ envelope by its fate.
 | `__compositeStep` | revived: the composite is resolved (J2 F-Call), then `.step` is read off the real result (L6.5) |
 | `__symbol` | revived: the text must match a simple dotted chain; its root resolves through the file's imports and the rest is real property access (L6.2) |
 
-In the `data-host` profile (F-Profile-DataHost, objective.md) none of these
-fates runs. Revival is serialization, every envelope is the output, and the
-host's serialization mapping is what turns it into the artifact.
+None of these fates runs in the `data-host` profile (F-Profile-DataHost,
+objective.md). That profile treats revival as serialization: the output is
+the envelopes themselves, and the host's serialization mapping is what turns
+them into the artifact.
 
 **Exactly one envelope survives to serialization: `__attrRef`.** The other
 five must never reach a serializer. An implementation that emits a
@@ -72,15 +73,15 @@ Revival carries a flag `requireLiveRefs`.
   resource's props (L6.9). A composite stores its props rather than
   inspecting them and the serializer resolves the envelope by name.
 
-So the same `v` is valid in one position and a rejection in another. A
+The same `v` is therefore valid in one position and a rejection in another. A
 specification of the domain alone does not capture this; the rule is part of
 the domain.
 
 ## F-Val-Live (liveness)
 
-A value *carries a live object* iff it, or anything reachable through plain
-objects and arrays, has a prototype other than `Object`, `Array`, or `null`,
-or is a function (`carriesLiveObject`, L4.5).
+A value *carries a live object* iff it is a function or has a prototype other
+than `Object`, `Array` or `null`, or anything reachable from it through plain
+objects and arrays does (`carriesLiveObject`, L4.5).
 
 Live objects reached through cross-file resolution, an `AttrRef` instance, a
 `Declarable`, a `CompositeInstance`, an `Intrinsic` instance, **pass through
@@ -124,8 +125,8 @@ whose contract is selective-by-omission depends on.
 
 Emission is where the key is dropped, and an `undefined` array element becomes
 `null` there, for both JSON and YAML, because YAML is round-tripped through
-the JSON emitter. For a lexicon that serializes YAML itself, the rule is that
-serializer's own.
+the JSON emitter. A lexicon that serializes YAML itself follows that
+serializer's own rule.
 
 ## F-Val-Symbol-Scope (where `__symbol` may appear)
 
diff --git a/spec/verdict.md b/spec/verdict.md
index 75e97d0..1342666 100644
--- a/spec/verdict.md
+++ b/spec/verdict.md
@@ -183,7 +183,7 @@ or a composite instance (a live object, F-Val-Live), `n` is bound to it for
 the evaluation of that argument. The binding is the one F-Eval-CallLocal
 gives a parameter. `n` is set in `externals` and removed from `consts`. F-Eval-Ident step 3
 then reads the instance and two reads of `n` are one object.
-When the call refuses or returns anything else, `n` stays as it was, and
+If the call refuses or returns anything else, `n` stays as it was and
 F-Eval-Ident re-folds the initializer and rejects. A read outside such an
 argument (an object literal at a declarator, say) is still J1's rejection. Inside an interpreted factory body no read qualifies.
 
@@ -213,6 +213,6 @@ call site with the callee's file and position in the message.
 ### What J2 does not decide
 
 Whether `f` *finally* folds. A file with `B, ι ⊢ f ⇓ fold(X, L)` may still be
-`run` after J3, because a file it imports runs (forward taint) or because a
-file it captured from runs (backward taint). J2's `fold` is a proposal; J3
+`run` after J3, because a file it imports runs (forward taint) or a file it
+captured from runs (backward taint). J2's `fold` is a proposal; J3
 disposes.