Skip to content

Symbolic derivations#

Workspace is the vocabulary a derivation is written against: a sequential list of typed steps, each either a real SymPy computation with a verdict (CONFIRMED / REFUTED / INCONCLUSIVE) or an explicitly recorded assumption (ASSERTED).

The split is the point. Anything SymPy can adjudicate is checked mechanically and carries its verdict; anything it cannot—an ansatz, a physical claim, an unverified relation—is recorded as an assumption rather than blurred into the derivation. A reader of the rendered result can always tell which is which.

This is what MathExpertAgent writes when a run needs an analytical result rather than a measured one.

adda.Workspace #

Records a derivation as a sequential list of typed steps.

Source code in src/adda/_src/epistemics/math_dsl.py 
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
class Workspace:
    """Records a derivation as a sequential list of typed steps."""

    def __init__(self, name: str) -> None:
        self.name = name
        self._steps: list[dict] = []
        _sp_random.seed(_DETERMINISM_SEED)

    # -- vocabulary: declaring symbols/functions -----------------------
    def symbols(self, names: str, **assumptions) -> tuple[sp.Symbol, ...]:
        syms = sp.symbols(names, **assumptions)
        if isinstance(syms, sp.Symbol):
            return (syms,)
        return tuple(syms)

    def function(self, name: str, *args):
        return sp.Function(name)(*args)

    # -- the one unverified-claim primitive -----------------------------
    def assume(
        self,
        name: str,
        statement: str,
        expr=None,
        symbolic_effect: str | None = None,
    ) -> None:
        """Record a claim SymPy never adjudicates. Verdict is always
        ``"ASSERTED"`` — an ansatz (pass `expr`), a scaling/truncation
        argument (pass `symbolic_effect`), or a bare physical claim."""
        latex = None
        if expr is not None:
            if isinstance(expr, dict):
                latex = r" \\ ".join(f"{k} = {_latex(v)}" for k, v in expr.items())
            else:
                latex = _latex(expr)
        self._steps.append({
            "name": name,
            "type": "assume",
            "verdict": "ASSERTED",
            "statement": statement,
            "symbolic_effect": symbolic_effect,
            "latex": latex,
            "derived_from": [],
        })

    # -- verified computations -------------------------------------------
    def check_equals(self, name: str, lhs, rhs, derived_from=()) -> str:
        """CONFIRMED if (lhs - rhs) simplifies to / is proven equal to 0;
        REFUTED if proven not equal; INCONCLUSIVE if SymPy can't decide
        (``.equals()`` returning `None` — never coerced to either pole)."""
        residual = sp.simplify(lhs - rhs)
        if residual == 0:
            verdict = "CONFIRMED"
        else:
            decided = (lhs - rhs).equals(0)
            if decided is True:
                verdict = "CONFIRMED"
            elif decided is False:
                verdict = "REFUTED"
            else:
                verdict = "INCONCLUSIVE"
        self._steps.append({
            "name": name,
            "type": "check_equals",
            "verdict": verdict,
            "latex": f"{_latex(lhs)} = {_latex(rhs)}",
            "residual": str(residual) if verdict != "CONFIRMED" else None,
            "derived_from": list(derived_from),
        })
        return verdict

    def check_holds(self, name: str, predicate, assumptions=None, derived_from=()) -> str:
        """Same three-valued verdict as check_equals, via SymPy's assumptions
        engine (`ask`) instead of equality — a domain/inequality claim is not
        an equality claim and check_equals cannot express it."""
        result = ask(predicate, assumptions) if assumptions is not None else ask(predicate)
        verdict = "CONFIRMED" if result is True else "REFUTED" if result is False else "INCONCLUSIVE"
        self._steps.append({
            "name": name,
            "type": "check_holds",
            "verdict": verdict,
            "latex": _latex(predicate),
            "residual": None,
            "derived_from": list(derived_from),
        })
        return verdict

    def check_dimensions(self, name: str, lhs, rhs, derived_from=()) -> str:
        """Unit-homogeneity check via the dimension SYSTEM's own equivalence
        (`equivalent_dims`), not raw subtraction of dimensional expressions —
        two dimensionally-equal quantities can have syntactically different
        dimensional expressions (a named unit like `newton` reduces to a
        symbol, a built-up expression reduces to `length*mass/time**2`)."""
        dimsys = SI.get_dimension_system()
        d_lhs = SI.get_dimensional_expr(lhs)
        d_rhs = SI.get_dimensional_expr(rhs)
        verdict = "CONFIRMED" if dimsys.equivalent_dims(d_lhs, d_rhs) else "REFUTED"
        self._steps.append({
            "name": name,
            "type": "check_dimensions",
            "verdict": verdict,
            "latex": f"[{_latex(lhs)}] = [{_latex(rhs)}]",
            "residual": None,
            "derived_from": list(derived_from),
        })
        return verdict

    def truncate_series(self, name: str, expr, small_param, order: int, derived_from=()):
        """Perturbation/asymptotic truncation — not expressible via
        check_equals/substitution alone. A computation, not a checked claim:
        verdict is None."""
        truncated = expr.series(small_param, 0, order).removeO()
        self._steps.append({
            "name": name,
            "type": "truncate_series",
            "verdict": None,
            "latex": _latex(truncated),
            "residual": None,
            "derived_from": list(derived_from),
        })
        return truncated

    def solve_ode(self, name: str, expr, func, ics=None, derived_from=()):
        """Integration with an initial/boundary condition (`dsolve`-based) —
        algebraically distinct from algebraic solving. A computation, not a
        checked claim: verdict is None."""
        solved = sp.dsolve(expr, func, ics=ics) if ics is not None else sp.dsolve(expr, func)
        self._steps.append({
            "name": name,
            "type": "solve_ode",
            "verdict": None,
            "latex": _latex(solved),
            "residual": None,
            "derived_from": list(derived_from),
        })
        return solved

    # -- query utility, not a recorded step -----------------------------
    def coefficient(self, expr, term):
        return expr.coeff(term)

    # -- interoperability output -----------------------------------------
    def render_latex(self, path: str) -> None:
        """One block per step, in call order — the sequential document a
        human or another agent reads directly."""
        lines = []
        for step in self._steps:
            lines.append(f"% {step['name']} ({step['type']}, {step['verdict']})")
            if step["type"] == "assume":
                lines.append(step["statement"])
                if step["symbolic_effect"]:
                    lines.append(f"% effect: {step['symbolic_effect']}")
            if step["latex"]:
                lines.append(f"\\[{step['latex']}\\]")
            lines.append("")
        with open(path, "w", encoding="utf-8") as f:
            f.write("\n".join(lines))

    def write_summary(self, path: str) -> None:
        """The interoperability contract: a consumer parses this without
        importing SymPy or reading the .py source at all.

        ``{"schema", "workspace", "counts", "steps"}``, where each step is
        ``{name, type, verdict, statement, latex, residual, derived_from}``.

        Three deliberate properties (run 20260912T142229 motivated all three):

        ``schema``  The file names its own format. Two consumers — the
            math_expert comparing two editions, and the critic auditing them —
            independently guessed the envelope and had to sniff it with an
            isinstance() guard. A record that does not say what it is forces
            every reader to infer it, and a later change breaks them silently
            instead of loudly.
        ``counts``  The verdict tally, computed once where the verdicts are
            authoritative. Every downstream consumer was recomputing it by
            hand and then narrating the result in prose, which puts an
            arithmetic step between the evidence and the claim. ``unchecked``
            counts steps SymPy never adjudicates (truncate_series, solve_ode:
            verdict ``None``); ASSERTED is its own bucket, not a check.
        ``residual``  The evidence for a non-CONFIRMED verdict. Without it the
            contract holds for the steps that passed and fails for exactly the
            steps a skeptical reader needs to examine.
        """
        steps = [
            {
                "name": s["name"],
                "type": s["type"],
                "verdict": s["verdict"],
                "statement": s.get("statement"),
                "latex": s["latex"],
                "residual": s.get("residual"),
                "derived_from": s["derived_from"],
            }
            for s in self._steps
        ]
        counts = {v: 0 for v in ("CONFIRMED", "REFUTED", "INCONCLUSIVE", "ASSERTED")}
        counts["unchecked"] = 0
        for s in steps:
            counts["unchecked" if s["verdict"] is None else s["verdict"]] += 1
        doc = {
            "schema": SUMMARY_SCHEMA,
            "workspace": self.name,
            "counts": counts,
            "steps": steps,
        }
        with open(path, "w", encoding="utf-8") as f:
            json.dump(doc, f, indent=2)
        self._append_history(path, doc)

    @staticmethod
    def _append_history(path: str, doc: dict) -> None:
        """Append this execution's summary to a sibling ``.history.jsonl``.

        A derivation script is edited and rerun until its checks pass, and
        every rerun builds a fresh Workspace and overwrites the summary. So a
        check that came back INCONCLUSIVE, prompted a correction, and then
        CONFIRMED leaves exactly the same trace as one that passed on the
        first try: none. That is the most informative event in the derivation
        — it is the evidence that a result was earned rather than assumed —
        and it was the one event the record could not hold.

        This is durability of evidence, not a claim about what a verdict
        means: nothing here changes a verdict, a count, or what the agent
        must do. The summary file remains the current state and the single
        thing any consumer reads; the journal is additive and write-only.

        NOT the JSONL call-log that spec 10 considered and dropped. That one
        replaced the .py script as the source of truth and needed bespoke
        code to replay it — dropped because a real derivation is linear and
        running the script top to bottom already IS the replay, which is
        still right. This appends finished summary documents; there is
        nothing to replay and the script stays the document.

        Never fatal: the summary is the contract and is already on disk by
        the time this runs. A journal that cannot be written costs a warning,
        not the derivation.
        """
        try:
            entry = {"written_at": _now_iso(), **doc}
            with open(
                Path(path).with_suffix(".history.jsonl"), "a", encoding="utf-8"
            ) as f:
                # One compact line per execution: a short single write keeps
                # concurrent appends from interleaving mid-record.
                f.write(json.dumps(entry, separators=(",", ":")) + "\n")
        except OSError as exc:
            log.warning("could not append derivation history for %s: %s", path, exc)
name = name instance-attribute #
_steps: list[dict] = [] instance-attribute #
symbols(names: str, **assumptions) -> tuple[sp.Symbol, ...] #
Source code in src/adda/_src/epistemics/math_dsl.py 
65
66
67
68
69
def symbols(self, names: str, **assumptions) -> tuple[sp.Symbol, ...]:
    syms = sp.symbols(names, **assumptions)
    if isinstance(syms, sp.Symbol):
        return (syms,)
    return tuple(syms)
function(name: str, *args) #
Source code in src/adda/_src/epistemics/math_dsl.py 
71
72
def function(self, name: str, *args):
    return sp.Function(name)(*args)
assume(name: str, statement: str, expr=None, symbolic_effect: str | None = None) -> None #

Record a claim SymPy never adjudicates. Verdict is always "ASSERTED" — an ansatz (pass expr), a scaling/truncation argument (pass symbolic_effect), or a bare physical claim.

Source code in src/adda/_src/epistemics/math_dsl.py 
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
def assume(
    self,
    name: str,
    statement: str,
    expr=None,
    symbolic_effect: str | None = None,
) -> None:
    """Record a claim SymPy never adjudicates. Verdict is always
    ``"ASSERTED"`` — an ansatz (pass `expr`), a scaling/truncation
    argument (pass `symbolic_effect`), or a bare physical claim."""
    latex = None
    if expr is not None:
        if isinstance(expr, dict):
            latex = r" \\ ".join(f"{k} = {_latex(v)}" for k, v in expr.items())
        else:
            latex = _latex(expr)
    self._steps.append({
        "name": name,
        "type": "assume",
        "verdict": "ASSERTED",
        "statement": statement,
        "symbolic_effect": symbolic_effect,
        "latex": latex,
        "derived_from": [],
    })
check_equals(name: str, lhs, rhs, derived_from=()) -> str #

CONFIRMED if (lhs - rhs) simplifies to / is proven equal to 0; REFUTED if proven not equal; INCONCLUSIVE if SymPy can't decide (.equals() returning None — never coerced to either pole).

Source code in src/adda/_src/epistemics/math_dsl.py 
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
def check_equals(self, name: str, lhs, rhs, derived_from=()) -> str:
    """CONFIRMED if (lhs - rhs) simplifies to / is proven equal to 0;
    REFUTED if proven not equal; INCONCLUSIVE if SymPy can't decide
    (``.equals()`` returning `None` — never coerced to either pole)."""
    residual = sp.simplify(lhs - rhs)
    if residual == 0:
        verdict = "CONFIRMED"
    else:
        decided = (lhs - rhs).equals(0)
        if decided is True:
            verdict = "CONFIRMED"
        elif decided is False:
            verdict = "REFUTED"
        else:
            verdict = "INCONCLUSIVE"
    self._steps.append({
        "name": name,
        "type": "check_equals",
        "verdict": verdict,
        "latex": f"{_latex(lhs)} = {_latex(rhs)}",
        "residual": str(residual) if verdict != "CONFIRMED" else None,
        "derived_from": list(derived_from),
    })
    return verdict
check_holds(name: str, predicate, assumptions=None, derived_from=()) -> str #

Same three-valued verdict as check_equals, via SymPy's assumptions engine (ask) instead of equality — a domain/inequality claim is not an equality claim and check_equals cannot express it.

Source code in src/adda/_src/epistemics/math_dsl.py 
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
def check_holds(self, name: str, predicate, assumptions=None, derived_from=()) -> str:
    """Same three-valued verdict as check_equals, via SymPy's assumptions
    engine (`ask`) instead of equality — a domain/inequality claim is not
    an equality claim and check_equals cannot express it."""
    result = ask(predicate, assumptions) if assumptions is not None else ask(predicate)
    verdict = "CONFIRMED" if result is True else "REFUTED" if result is False else "INCONCLUSIVE"
    self._steps.append({
        "name": name,
        "type": "check_holds",
        "verdict": verdict,
        "latex": _latex(predicate),
        "residual": None,
        "derived_from": list(derived_from),
    })
    return verdict
check_dimensions(name: str, lhs, rhs, derived_from=()) -> str #

Unit-homogeneity check via the dimension SYSTEM's own equivalence (equivalent_dims), not raw subtraction of dimensional expressions — two dimensionally-equal quantities can have syntactically different dimensional expressions (a named unit like newton reduces to a symbol, a built-up expression reduces to length*mass/time**2).

Source code in src/adda/_src/epistemics/math_dsl.py 
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
def check_dimensions(self, name: str, lhs, rhs, derived_from=()) -> str:
    """Unit-homogeneity check via the dimension SYSTEM's own equivalence
    (`equivalent_dims`), not raw subtraction of dimensional expressions —
    two dimensionally-equal quantities can have syntactically different
    dimensional expressions (a named unit like `newton` reduces to a
    symbol, a built-up expression reduces to `length*mass/time**2`)."""
    dimsys = SI.get_dimension_system()
    d_lhs = SI.get_dimensional_expr(lhs)
    d_rhs = SI.get_dimensional_expr(rhs)
    verdict = "CONFIRMED" if dimsys.equivalent_dims(d_lhs, d_rhs) else "REFUTED"
    self._steps.append({
        "name": name,
        "type": "check_dimensions",
        "verdict": verdict,
        "latex": f"[{_latex(lhs)}] = [{_latex(rhs)}]",
        "residual": None,
        "derived_from": list(derived_from),
    })
    return verdict
truncate_series(name: str, expr, small_param, order: int, derived_from=()) #

Perturbation/asymptotic truncation — not expressible via check_equals/substitution alone. A computation, not a checked claim: verdict is None.

Source code in src/adda/_src/epistemics/math_dsl.py 
163
164
165
166
167
168
169
170
171
172
173
174
175
176
def truncate_series(self, name: str, expr, small_param, order: int, derived_from=()):
    """Perturbation/asymptotic truncation — not expressible via
    check_equals/substitution alone. A computation, not a checked claim:
    verdict is None."""
    truncated = expr.series(small_param, 0, order).removeO()
    self._steps.append({
        "name": name,
        "type": "truncate_series",
        "verdict": None,
        "latex": _latex(truncated),
        "residual": None,
        "derived_from": list(derived_from),
    })
    return truncated
solve_ode(name: str, expr, func, ics=None, derived_from=()) #

Integration with an initial/boundary condition (dsolve-based) — algebraically distinct from algebraic solving. A computation, not a checked claim: verdict is None.

Source code in src/adda/_src/epistemics/math_dsl.py 
178
179
180
181
182
183
184
185
186
187
188
189
190
191
def solve_ode(self, name: str, expr, func, ics=None, derived_from=()):
    """Integration with an initial/boundary condition (`dsolve`-based) —
    algebraically distinct from algebraic solving. A computation, not a
    checked claim: verdict is None."""
    solved = sp.dsolve(expr, func, ics=ics) if ics is not None else sp.dsolve(expr, func)
    self._steps.append({
        "name": name,
        "type": "solve_ode",
        "verdict": None,
        "latex": _latex(solved),
        "residual": None,
        "derived_from": list(derived_from),
    })
    return solved
coefficient(expr, term) #
Source code in src/adda/_src/epistemics/math_dsl.py 
194
195
def coefficient(self, expr, term):
    return expr.coeff(term)
render_latex(path: str) -> None #

One block per step, in call order — the sequential document a human or another agent reads directly.

Source code in src/adda/_src/epistemics/math_dsl.py 
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
def render_latex(self, path: str) -> None:
    """One block per step, in call order — the sequential document a
    human or another agent reads directly."""
    lines = []
    for step in self._steps:
        lines.append(f"% {step['name']} ({step['type']}, {step['verdict']})")
        if step["type"] == "assume":
            lines.append(step["statement"])
            if step["symbolic_effect"]:
                lines.append(f"% effect: {step['symbolic_effect']}")
        if step["latex"]:
            lines.append(f"\\[{step['latex']}\\]")
        lines.append("")
    with open(path, "w", encoding="utf-8") as f:
        f.write("\n".join(lines))
write_summary(path: str) -> None #

The interoperability contract: a consumer parses this without importing SymPy or reading the .py source at all.

{"schema", "workspace", "counts", "steps"}, where each step is {name, type, verdict, statement, latex, residual, derived_from}.

Three deliberate properties (run 20260912T142229 motivated all three):

schema The file names its own format. Two consumers — the math_expert comparing two editions, and the critic auditing them — independently guessed the envelope and had to sniff it with an isinstance() guard. A record that does not say what it is forces every reader to infer it, and a later change breaks them silently instead of loudly. counts The verdict tally, computed once where the verdicts are authoritative. Every downstream consumer was recomputing it by hand and then narrating the result in prose, which puts an arithmetic step between the evidence and the claim. unchecked counts steps SymPy never adjudicates (truncate_series, solve_ode: verdict None); ASSERTED is its own bucket, not a check. residual The evidence for a non-CONFIRMED verdict. Without it the contract holds for the steps that passed and fails for exactly the steps a skeptical reader needs to examine.

Source code in src/adda/_src/epistemics/math_dsl.py 
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
def write_summary(self, path: str) -> None:
    """The interoperability contract: a consumer parses this without
    importing SymPy or reading the .py source at all.

    ``{"schema", "workspace", "counts", "steps"}``, where each step is
    ``{name, type, verdict, statement, latex, residual, derived_from}``.

    Three deliberate properties (run 20260912T142229 motivated all three):

    ``schema``  The file names its own format. Two consumers — the
        math_expert comparing two editions, and the critic auditing them —
        independently guessed the envelope and had to sniff it with an
        isinstance() guard. A record that does not say what it is forces
        every reader to infer it, and a later change breaks them silently
        instead of loudly.
    ``counts``  The verdict tally, computed once where the verdicts are
        authoritative. Every downstream consumer was recomputing it by
        hand and then narrating the result in prose, which puts an
        arithmetic step between the evidence and the claim. ``unchecked``
        counts steps SymPy never adjudicates (truncate_series, solve_ode:
        verdict ``None``); ASSERTED is its own bucket, not a check.
    ``residual``  The evidence for a non-CONFIRMED verdict. Without it the
        contract holds for the steps that passed and fails for exactly the
        steps a skeptical reader needs to examine.
    """
    steps = [
        {
            "name": s["name"],
            "type": s["type"],
            "verdict": s["verdict"],
            "statement": s.get("statement"),
            "latex": s["latex"],
            "residual": s.get("residual"),
            "derived_from": s["derived_from"],
        }
        for s in self._steps
    ]
    counts = {v: 0 for v in ("CONFIRMED", "REFUTED", "INCONCLUSIVE", "ASSERTED")}
    counts["unchecked"] = 0
    for s in steps:
        counts["unchecked" if s["verdict"] is None else s["verdict"]] += 1
    doc = {
        "schema": SUMMARY_SCHEMA,
        "workspace": self.name,
        "counts": counts,
        "steps": steps,
    }
    with open(path, "w", encoding="utf-8") as f:
        json.dump(doc, f, indent=2)
    self._append_history(path, doc)
_append_history(path: str, doc: dict) -> None staticmethod #

Append this execution's summary to a sibling .history.jsonl.

A derivation script is edited and rerun until its checks pass, and every rerun builds a fresh Workspace and overwrites the summary. So a check that came back INCONCLUSIVE, prompted a correction, and then CONFIRMED leaves exactly the same trace as one that passed on the first try: none. That is the most informative event in the derivation — it is the evidence that a result was earned rather than assumed — and it was the one event the record could not hold.

This is durability of evidence, not a claim about what a verdict means: nothing here changes a verdict, a count, or what the agent must do. The summary file remains the current state and the single thing any consumer reads; the journal is additive and write-only.

NOT the JSONL call-log that spec 10 considered and dropped. That one replaced the .py script as the source of truth and needed bespoke code to replay it — dropped because a real derivation is linear and running the script top to bottom already IS the replay, which is still right. This appends finished summary documents; there is nothing to replay and the script stays the document.

Never fatal: the summary is the contract and is already on disk by the time this runs. A journal that cannot be written costs a warning, not the derivation.

Source code in src/adda/_src/epistemics/math_dsl.py 
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
@staticmethod
def _append_history(path: str, doc: dict) -> None:
    """Append this execution's summary to a sibling ``.history.jsonl``.

    A derivation script is edited and rerun until its checks pass, and
    every rerun builds a fresh Workspace and overwrites the summary. So a
    check that came back INCONCLUSIVE, prompted a correction, and then
    CONFIRMED leaves exactly the same trace as one that passed on the
    first try: none. That is the most informative event in the derivation
    — it is the evidence that a result was earned rather than assumed —
    and it was the one event the record could not hold.

    This is durability of evidence, not a claim about what a verdict
    means: nothing here changes a verdict, a count, or what the agent
    must do. The summary file remains the current state and the single
    thing any consumer reads; the journal is additive and write-only.

    NOT the JSONL call-log that spec 10 considered and dropped. That one
    replaced the .py script as the source of truth and needed bespoke
    code to replay it — dropped because a real derivation is linear and
    running the script top to bottom already IS the replay, which is
    still right. This appends finished summary documents; there is
    nothing to replay and the script stays the document.

    Never fatal: the summary is the contract and is already on disk by
    the time this runs. A journal that cannot be written costs a warning,
    not the derivation.
    """
    try:
        entry = {"written_at": _now_iso(), **doc}
        with open(
            Path(path).with_suffix(".history.jsonl"), "a", encoding="utf-8"
        ) as f:
            # One compact line per execution: a short single write keeps
            # concurrent appends from interleaving mid-record.
            f.write(json.dumps(entry, separators=(",", ":")) + "\n")
    except OSError as exc:
        log.warning("could not append derivation history for %s: %s", path, exc)