paper, README: clear the remaining sentences 0.5.1 baseline

README.md

@@ -6,7 +6,7 @@ The subset is the part of TypeScript whose value is fixed by its source: literal
 
 ## Status
 
-Every part of the mechanism has a normative draft under `spec/`. One identifier vocabulary covers them (`S-*` for shape rules, `F-*` for fold rules). A decision-point inventory of 112 rows cites those rules and is gated in CI. A reference implementation covers J1 to J3 and revival; `packages/reference/CAVEATS.md` says what it does not. chant is cross-checked against it from the published package, on the fixtures and on chant's whole example corpus. Fixture coverage is 136 of 139 rules; `spec/fixtures/UNCOVERED.md` lists the rest with a reason each and may only shrink.
+Every part of the mechanism has a normative draft under `spec/`. One identifier vocabulary covers them (`S-*` for shape rules, `F-*` for fold rules). A decision-point inventory of 112 rows cites those rules and is gated in CI. A reference implementation covers J1 to J3 and revival; `packages/reference/CAVEATS.md` says what it does not. The published chant package is cross-checked against it over the fixtures and chant's whole example corpus. Fixture coverage is 136 of 139 rules; `spec/fixtures/UNCOVERED.md` lists the rest with a reason each and may only shrink.
 
 ## Layout
 

paper/discussion.md

@@ -16,7 +16,7 @@ Nothing answers "will this produce the same output tomorrow" short of
 declining to run the source. A run returns a value and says nothing about
 where the value came from, so no inspection of the artifact recovers the
 difference. The security consequence is real and downstream. A build that
-reproduces from source alone is one that never executed the source. Pitching
+reproduces from source alone is one whose source never ran. Pitching
 it the other way round invites a substitution that does not hold.
 
 ## What is unresolved
@@ -35,7 +35,7 @@ A specification that presented these as designed would be easier to read and les
 
 The identity theorem is the paper's center, so here is what would break it. Three things would.
 
-**A single fold/run disagreement on a mixed build.** The differential requires identical errors and byte-identical output for every corpus entry, including the twelve with at least one file that falls back. One disagreement there is either a bug in the fixpoint or a gap in the argument, and the entry would name itself.
+**A single fold/run disagreement on a mixed build**. The differential requires identical errors and byte-identical output for every corpus entry, including the twelve with at least one file that falls back. One disagreement there is either a bug in the fixpoint or a gap in the argument, and the entry would name itself.
 
 **An entity reachable by two paths with different verdicts.** The theorem's case analysis rules this out given `F-Memo` and `F-Count`. Two implementation choices would produce it anyway: memoising per referrer instead of per build, or invoking a composite once per member access. The corpus would not necessarily catch either.
 

paper/enables.md

@@ -4,15 +4,15 @@ Draft for #87. The other sections say what the fold is. This one says what it is
 
 ## Synthesis with no execution
 
-A file in the subset becomes its artifact by being read. Nothing runs, so the artifact is a function of the source and the build-parameter binding and nothing else. The same file yields the same artifact on any machine and in any evaluator, whatever language the evaluator is written in. A reviewer reading a diff sees exactly what will ship. The user never meets the fold as a mechanism; they meet it as a lint that says at the keystroke whether the file is data and points at the line that makes it not data. That lint is the shape classifier of `grammar.md`, and it needs no evaluator to run. `F-NoOwnExecution` is the rule, and chant's execution-boundary profile (`measurements.md`) is the measurement.
+A file in the subset becomes its artifact by being read. Nothing runs, so the artifact is a function of the source and the build-parameter binding and nothing else. Any machine and any evaluator get the same artifact from the same file, whatever language the evaluator is written in. A reviewer reading a diff sees exactly what will ship. The user never meets the fold as a mechanism; they meet it as a lint that says at the keystroke whether the file is data and points at the line that makes it not data. That lint is the shape classifier of `grammar.md`, and it needs no evaluator to run. `F-NoOwnExecution` is the rule, and chant's execution-boundary profile (`measurements.md`) is the measurement.
 
 ## Semantic rules over values
 
 A syntax linter sees tokens and can say a key is misspelt. A configuration language with constraints in the type can say a port is out of range. Neither can say that two fields of one resource contradict each other, and neither can say that a resource in one file makes a resource in another file incoherent. They lack the values of every file in the build before anything is emitted. The fold does. A rule that runs over folded values is a pure function of its input, deterministic and free of I/O, which is what lets it run in an editor, and it sees the same data in the editor that it sees in CI, because the data is a function of the source. Two phases follow from this: rules over the declared values before serialization, and rules over the emitted artifact after. chant's lexicons carry the first kind and its post-synth checks the second; a governance tool built on the same evaluator carries both without naming them, in its config loader and in its plan guardrails. The contract those rules run under is `rules.md` (spec `1.4`). It names the input a check sees and when it runs, what a check may do and what a finding carries, and who supplies it. Fixtures for it wait on a harness hook (typescript-as-data#101).
 
 ## Round-trip generation
 
-The fold goes from source to data. A generator goes from data to source. Composed, an existing artifact or a live system becomes source that folds back to exactly what it came from, `fold(generate(v)) = v`. This is where the choice of a general-purpose language stops being taste and becomes correctness. A generator decides what each value is, and each decision needs a source form the subset can express and the fold can reverse. A literal is a literal. A value that is another resource's attribute is `bucket.Arn`, which `F-Eval-Member` step 1 turns back into an attribute reference. A repetition across forty resources is one `const`, spread where it is used, which `F-Eval-Object` folds back to the same forty objects. YAML cannot express the second or the third; a configuration language can, but then the source is no longer the artifact's own shape. chant has three generators through one pipeline and a round-trip suite for one target. The property itself is stated as a forward reference (typescript-as-data#80): every value in the domain has a source form that folds to it, and a generator's output is held to folding to its input.
+The fold goes from source to data and a generator goes the other way. Composed, an existing artifact or a live system becomes source that folds back to exactly what it came from, `fold(generate(v)) = v`. This is where the choice of a general-purpose language stops being taste and becomes correctness. A generator decides what each value is, and each decision needs a source form the subset can express and the fold can reverse. A literal is a literal. A value that is another resource's attribute is `bucket.Arn`, which `F-Eval-Member` step 1 turns back into an attribute reference. A repetition across forty resources is one `const`, spread where it is used, which `F-Eval-Object` folds back to the same forty objects. YAML cannot express the second or the third; a configuration language can, but then the source is no longer the artifact's own shape. chant has three generators through one pipeline and a round-trip suite for one target. The property itself is stated as a forward reference (typescript-as-data#80): every value in the domain has a source form that folds to it, and a generator's output is held to folding to its input.
 
 ## Which profile each needs
 

paper/introduction.md

@@ -14,25 +14,25 @@ Graceful fallback from static evaluation to execution is not itself new; compile
 
 ## The problem
 
-Configuration as data is auditable: every value traces to a line of source, and the build makes no network call and holds no credential. Configuration as code is expressive: types, imports, refactoring, a language people already know. Existing designs pick one. A configuration language gives up the general-purpose ecosystem; a program that emits configuration gives up the property that made data auditable, because the graph exists only as the output of a run.
+Configuration as data is auditable: every value traces to a line of source, and the build makes no network call and holds no credential. As code, configuration is expressive: types, imports and refactoring come with a language people already know. Existing designs pick one. Choosing a configuration language gives up the general-purpose ecosystem; a program that emits configuration gives up the property that made data auditable, because the graph exists only as the output of a run.
 
 The fragment approach promises both. Its difficulty is not defining the fragment, which is routine, but defining the edge.
 
 ## The edge is the contribution
 
 A total language never has to answer what happens to source it cannot evaluate, because that source does not compile. A system with a fallback must answer it, and three obligations follow.
 
-**The two paths must agree.** Folding a file and running it must be observationally equivalent, at a fixed build-parameter binding. Stating this precisely means stating what still executes when a file folds: the file's own statements do not, but resolving a name to its real constructor and invoking it does.
+**The two paths must agree**. Folding a file and running it must be observationally equivalent, at a fixed build-parameter binding. Stating this precisely means stating what still executes when a file folds: the file's own statements do not, but resolving a name to its real constructor and invoking it does.
 
-**The decision must be total per unit.** A file folds entirely or runs entirely. Partial folding would mean holding a half-built namespace.
+**The decision must be total per unit**. A file folds entirely or runs entirely. Partial folding would mean holding a half-built namespace.
 
-**Identity must survive the boundary.** This is the obligation with no precedent we found. If one file folds and another runs, and both refer to an entity the first produced, the build holds two objects for one entity. Attribute references cannot both receive a logical name; a reference to one silently inlines rather than referring. Every comparable system avoids this by construction: compile-time function execution copies values across its boundary, per-page rendering shares no runtime objects, and a whole-program partial evaluator has a single heap. Only a per-unit decision over a shared object graph has the problem at all.
+**Identity must survive the boundary**. This is the obligation with no precedent we found. If one file folds and another runs, and both refer to an entity the first produced, the build holds two objects for one entity. Attribute references cannot both receive a logical name; a reference to one silently inlines rather than referring. Every comparable system avoids this by construction: compile-time function execution copies values across its boundary, per-page rendering shares no runtime objects, and a whole-program partial evaluator has a single heap. Only a per-unit decision over a shared object graph has the problem at all.
 
 The answer is a fixpoint over the module graph, closed under two edges: a running file taints what it imports, and a file whose objects were captured taints the capturer. A third edge runs through calls rather than imports.
 
 ## What we provide
 
-A specification of the subset and its edge, as a grammar and four judgments with identified rules. A reference implementation of the expression layer, written from the specification text. A conformance suite in which every rule is cited by the fixtures that exercise it, and a ledger in which every decision point of a production implementation cites the rule that governs it. And measurements from that production implementation: a differential over 116 corpus entries requiring identical errors and byte-identical output, an execution-boundary measurement, and a build designed to make the fixpoint fire in both directions.
+A specification of the subset and its edge, as a grammar and four judgments with identified rules. A reference implementation of the expression layer, written from the specification text. A conformance suite in which every rule is cited by the fixtures that exercise it, and a ledger in which every decision point of a production implementation cites the rule that governs it. We also report measurements from that production implementation: a differential over 116 corpus entries requiring identical errors and byte-identical output, an execution-boundary measurement, and a build designed to make the fixpoint fire in both directions.
 
 ## What we do not claim