This notebook introduces a synthesis record over notebook 01’s traceability graph and notebook 02’s judgment ledger; after running it you can see, in one place, what has real bidirectional verification evidence, what has only one-sided evidence, how the model’s own strongest formal proof -- once found disconnected from any requirement -- is now tied to one by notebook 01’s own remediation, and what an accountable engineer would still have to decide before actually shipping this design.
State the distinction this whole notebook rests on before building anything: a completed traceability graph and a judgment ledger are not sign-off itself. Sign-off is a human, accountable act; a design’s own engineer decides, given everything the graph and the ledger show, whether to proceed. This notebook can show the inputs to that decision, honestly and within its own stated scope, but it cannot make the decision for anyone, and it does not try to. The record built below stays disposition = "pending", the same as every other record this tutorial has ever built (a standing rule of this tutorial): this chapter does not get to be the exception.
from pathlib import Path
import opensysml
from toaster.report import format_diagnostics
conn = opensysml.connect(version="v0.9.0")
source = Path("../../models/ch10-cumulative.sysml").read_text()
model = conn.load_from_content(source, strict=False)
assert model.ok, f"Model failed: {format_diagnostics(model.diagnostics)}"
Before assembling anything, a real negative control fitting this notebook’s own new record: does validate_record() reject a draft of it whose own counterevidence is empty? counterevidence is exactly the field this tutorial treats as load-bearing, and this check is real and mechanized, unlike a different rule discussed just below that no tool enforces.
from toaster.evidence import ReviewRecord, hash_content, validate_record
draft_missing_counterevidence = ReviewRecord(
identifier="AI-C10-DRAFT",
kind="asserted_inference",
claim="A draft of the synthesis record built below, missing its own counterevidence.",
model_ref="ToasterDemo",
content_hash=hash_content(source),
scope="ToasterDemo",
criteria="The same criteria the real record below states.",
premises=["a premise"],
rationale="Because the graph and the ledger say so.",
counterevidence="", # intentionally empty
disposition="pending",
record_kind="worked_example",
)
errors = validate_record(draft_missing_counterevidence, model=model)
assert errors == ["counterevidence is empty"], errors
print(f"Negative control ok: errors={errors}")
Negative control ok: errors=['counterevidence is empty']
validate_record() correctly rejects this: a real, mechanized floor actually catching something, the same check Chapter 9’s own placeholder record exercised. A different rule this tutorial follows just as strictly has no such mechanized floor: this tutorial forbids ever recording disposition="accepted", but reading src/toaster/evidence.py’s own validate_record() shows what it actually checks: identifier, claim, rationale and counterevidence non-empty, record_kind != "actual_review", at least one premise for an asserted_inference, and subject_ref present (resolving in the model and agreeing with any model-side tag, when a model is given) for asserted_context/asserted_solution or an asserted_inference with no premises -- never the disposition value itself. That gap is real and worth naming plainly, but it is not demonstrated here by constructing the forbidden value: this tutorial’s own rule against disposition="accepted" has no negative-control exception, so this point is made in prose only, never in code. Every record this notebook goes on to build keeps disposition="pending", checked explicitly at the end, not merely asserted.
With that settled, the two real inputs this synthesis draws on: notebook 01’s own coverage-and-orphan finding, recomputed directly below against the loaded model (each notebook in this tutorial loads and runs independently, so nothing here is assumed from memory), and a short summary of notebook 02’s own three-record ledger, hand-verified against that notebook’s own real, printed output rather than rebuilt a third time.
from toaster.query import ApiIndex, requirement_coverage, requirement_ties, tied_to_any_requirement
idx = ApiIndex(model)
coverage = {c["requirement"]: c for c in requirement_coverage(model, idx)}
delivered_energy_bounded = idx.by_qn["ToasterDemo::deliveredEnergyBoundedBySupply"]
ties = requirement_ties(model, "ToasterDemo::deliveredEnergyBoundedBySupply", idx)
tied_to_a_requirement = tied_to_any_requirement(model, "ToasterDemo::deliveredEnergyBoundedBySupply", idx)
print(f"heatGenerationReq: {coverage['ToasterDemo::heatGenerationReq']}")
print(f"timely: {coverage['ToasterDemo::timely']}")
print(f"energyConservationReq: {coverage['ToasterDemo::energyConservationReq']}")
print(f"deliveredEnergyBoundedBySupply tied to any requirement: {tied_to_a_requirement} ({ties})")
assert coverage["ToasterDemo::heatGenerationReq"]["covered"] is True
assert coverage["ToasterDemo::timely"]["covered"] is False
assert coverage["ToasterDemo::energyConservationReq"]["covered"] is False
assert tied_to_a_requirement
assert len(ties) == 1 and ties[0]["requirement"] == "ToasterDemo::EnergyConservationReq"heatGenerationReq: {'requirement': 'ToasterDemo::heatGenerationReq', 'satisfied_by': ['ToasterDemo::rated'], 'failed_by': ['ToasterDemo::weak'], 'covered': True}
timely: {'requirement': 'ToasterDemo::timely', 'satisfied_by': [], 'failed_by': ['ToasterDemo::slow'], 'covered': False}
energyConservationReq: {'requirement': 'ToasterDemo::energyConservationReq', 'satisfied_by': [], 'failed_by': [], 'covered': False}
deliveredEnergyBoundedBySupply tied to any requirement: True ([{'tying_element': 'ToasterDemo::EnergyConservationReq::c', 'field': 'subsets', 'requirement': 'ToasterDemo::EnergyConservationReq'}])
The same findings notebook 01 established, reproduced here directly: heatGenerationReq has real, bidirectional verification evidence (rated satisfies it, weak fails it); timely has only a one-sided negative claim and an unbound verify objective, no positive claim at all; and deliveredEnergyBoundedBySupply, the model’s own strongest formal proof, is now tied to energyConservationReq -- notebook 01’s own remediation for exactly the gap its traceability graph found there, confirmed above by the same check (Check B’s own subsetting hit, attributed to the DEFINITION). energyConservationReq’s own covered=False is not another gap of the same kind as timely’s: it is the deliberate, by-design result of this requirement being tied by subsetting an already-proved universal lemma rather than by any instance-level assert satisfy -- notebook 01’s own negative control shows directly why that idiom does not hold up here. Notebook 02’s own ledger is cited next by identifier and conclusion, not rebuilt a third time; its own fields were already verified verbatim there.
Notebook 01’s own judgment record, AC-C10 (kind="asserted_context"), frames how this tie should honestly be read: cited here by identifier and conclusion, not rebuilt a third time, the same way notebook 02’s own ledger is cited next.
ac_c10_summary = {"kind": "asserted_context", "engineering_conclusion": "undetermined"}
print(f"AC-C10: {ac_c10_summary}")
AC-C10: {'kind': 'asserted_context', 'engineering_conclusion': 'undetermined'}
Notebook 02’s own three-record ledger is cited next, the same way -- by identifier and conclusion, not rebuilt a third time.
ledger_summary = {
"AS-C06": {"kind": "asserted_solution", "engineering_conclusion": "undetermined"},
"AS-C08": {"kind": "asserted_solution", "engineering_conclusion": "supported"},
"AI-C06": {"kind": "asserted_inference", "engineering_conclusion": "undetermined"},
}
for identifier, summary in ledger_summary.items():
print(f"{identifier}: {summary}")
AS-C06: {'kind': 'asserted_solution', 'engineering_conclusion': 'undetermined'}
AS-C08: {'kind': 'asserted_solution', 'engineering_conclusion': 'supported'}
AI-C06: {'kind': 'asserted_inference', 'engineering_conclusion': 'undetermined'}
Notebook 01’s graph and notebook 02’s ledger are now both in hand. The rest of this notebook builds one new record synthesizing them, following the judgment-record construction zone: name each group of fields, narrate what it is for, print it, then assemble.
What is being claimed, and about what: the synthesis itself, not any single requirement or record.
claim = (
"Notebook 01's traceability graph and notebook 02's judgment ledger, taken "
"together, give an accountable engineer a real, honestly-scoped basis for "
"exercising sign-off judgment over this model as it stands: heatGenerationReq "
"is bidirectionally verified, timely traces to a real functional intent with "
"no positive verification at all, and the model's own strongest formal "
"evidence (deliveredEnergyBoundedBySupply), found disconnected from any "
"stated requirement by notebook 01's own traceability graph, is now tied to "
"energyConservationReq by subsetting, the requirement notebook 01 added "
"specifically to close that gap -- not by any assert-satisfy claim, which "
"notebook 01's own negative control showed does not hold up here. This "
"record synthesizes those findings; it does not itself constitute sign-off, "
"which remains a human, accountable act this tutorial can show the inputs "
"to but not perform."
)
model_ref = "ToasterDemo"
print(claim)
Notebook 01's traceability graph and notebook 02's judgment ledger, taken together, give an accountable engineer a real, honestly-scoped basis for exercising sign-off judgment over this model as it stands: heatGenerationReq is bidirectionally verified, timely traces to a real functional intent with no positive verification at all, and the model's own strongest formal evidence (deliveredEnergyBoundedBySupply), found disconnected from any stated requirement by notebook 01's own traceability graph, is now tied to energyConservationReq by subsetting, the requirement notebook 01 added specifically to close that gap -- not by any assert-satisfy claim, which notebook 01's own negative control showed does not hold up here. This record synthesizes those findings; it does not itself constitute sign-off, which remains a human, accountable act this tutorial can show the inputs to but not perform.
What standard this claim is checked against (appropriateness): confined to exactly what notebooks 01 and 02 established, nothing wider.
scope = (
"The three chains notebook 01's own traceability graph built (heatGenerationReq "
"and its bidirectional satisfy claims; timely and its one-sided negative claim "
"plus its unbound verify objective; deliveredEnergyBoundedBySupply, proved by "
"Z3, found tied to no requirement by notebook 01's own traceability graph, and "
"then tied to a new requirement, energyConservationReq, added by that same "
"notebook to close that gap by subsetting, not by satisfy), and the three "
"records notebook 02's own ledger reconstructed (AS-C06, AS-C08, AI-C06), plus "
"notebook 01's own AC-C10. Confined to what those two notebooks actually "
"established; not a claim about any part of the model neither notebook "
"touched."
)
criteria = (
"For each traced element: is there real, bidirectional verification evidence "
"(a positive AND a negative claim), only one-sided evidence, or none at all? "
"Does a proven formal property connect back to a stated requirement? Here it "
"now does, but only because notebook 01 closed a gap its own traceability "
"graph found (the inverse of a failure mode Douglas's own traceability "
"concern names: an unjustified widget, a design element with no requirement "
"behind it; here, evidence that briefly had no requirement in front of it) -- "
"and AC-C10 already names the honest limits of what that closure actually "
"establishes."
)
print(scope)
print(criteria)The three chains notebook 01's own traceability graph built (heatGenerationReq and its bidirectional satisfy claims; timely and its one-sided negative claim plus its unbound verify objective; deliveredEnergyBoundedBySupply, proved by Z3, found tied to no requirement by notebook 01's own traceability graph, and then tied to a new requirement, energyConservationReq, added by that same notebook to close that gap by subsetting, not by satisfy), and the three records notebook 02's own ledger reconstructed (AS-C06, AS-C08, AI-C06), plus notebook 01's own AC-C10. Confined to what those two notebooks actually established; not a claim about any part of the model neither notebook touched.
For each traced element: is there real, bidirectional verification evidence (a positive AND a negative claim), only one-sided evidence, or none at all? Does a proven formal property connect back to a stated requirement? Here it now does, but only because notebook 01 closed a gap its own traceability graph found (the inverse of a failure mode Douglas's own traceability concern names: an unjustified widget, a design element with no requirement behind it; here, evidence that briefly had no requirement in front of it) -- and AC-C10 already names the honest limits of what that closure actually establishes.
What is being taken as given: the three ledger records plus AC-C10, cited by identifier, and the coverage/tie results notebook 01 established, both already independently verified above and in notebook 02, not re-argued here.
premises = [
f"notebook 01's traceability graph: heatGenerationReq "
f"covered={coverage['ToasterDemo::heatGenerationReq']['covered']} "
f"(satisfied_by={coverage['ToasterDemo::heatGenerationReq']['satisfied_by']}, "
f"failed_by={coverage['ToasterDemo::heatGenerationReq']['failed_by']}); timely "
f"covered={coverage['ToasterDemo::timely']['covered']} "
f"(satisfied_by={coverage['ToasterDemo::timely']['satisfied_by']}, "
f"failed_by={coverage['ToasterDemo::timely']['failed_by']}, plus "
"TimelyToastTest's own unbound "
"verify objective); deliveredEnergyBoundedBySupply, found tied to no "
"requirement under two narrow, explicitly-named checks (satisfy-by-subject; "
"a direct subsets/redefines/references/referent reference from within a "
"RequirementDefinition/RequirementUsage's own body, exact-type owner only), "
f"is now tied to EnergyConservationReq (the definition) by subsetting ({ties}), "
"added by notebook 01 to close that gap -- not a claim that no other tie could "
f"exist by any conceivable mechanism, only that this one, real "
f"(tied_to_a_requirement={tied_to_a_requirement}), is closed.",
"AS-C06 (asserted_solution, Chapter 6): ResistanceCoil selected over a "
"combustion alternative; engineering_conclusion=undetermined, argued from a "
"domain premise, not a trade study.",
"AS-C08 (asserted_solution, Chapter 8): deliveredEnergyBoundedBySupply proved "
"by Z3; engineering_conclusion=supported, but the proof is a hand-restated "
"lemma, not a solver-checked reference to HeatGenerator's own "
"efficiencyBounded/deliveredEnergy.",
"AI-C06 (asserted_inference, Chapter 6): the level-2 heat-generation branch's "
"own stopping judgment; engineering_conclusion=undetermined, energyIn not "
"wired to any producer, HeatingAssembly not composed into any Toaster "
"candidate.",
"AC-C10 (asserted_context, Chapter 10): frames the energyConservationReq tie "
"honestly -- the subsetting mechanism is spec-legitimate (SS7.21.2) and the "
"requirement's own general motivation (energy conservation) is genuine, but "
"its own need was identified retroactively, after Chapter 8's proof, "
"specifically to close this chapter's own traceability gap; the tie is "
"purely structural (Check B alone), deliberately not reinforced by any "
"assert-satisfy claim -- confirmed by direct test to fail under "
"model.verify_satisfaction() regardless of which candidate is bound, and, "
"separately, confirmed by contrast that adding it back makes sysmlv2 "
"verify --solve reduce to the identical 'undecided, indeterminate over "
"unbound features' verdict every other requirement's own unbound required "
"constraint already gets in this model -- a real check, but one that still "
"resolves nothing, not the absence of a check -- so requirement_coverage()'s "
"own covered=False for it is correct and expected, not a residual gap.",
]
assumption_refs = [
"Toaster::cycleTime remains a settable, underived attribute (unchanged since "
"Chapter 2); this record does not assume it has been derived from anything."
]
for p in premises:
print(p)
print()
print(assumption_refs)notebook 01's traceability graph: heatGenerationReq covered=True (satisfied_by=['ToasterDemo::rated'], failed_by=['ToasterDemo::weak']); timely covered=False (satisfied_by=[], failed_by=['ToasterDemo::slow'], plus TimelyToastTest's own unbound verify objective); deliveredEnergyBoundedBySupply, found tied to no requirement under two narrow, explicitly-named checks (satisfy-by-subject; a direct subsets/redefines/references/referent reference from within a RequirementDefinition/RequirementUsage's own body, exact-type owner only), is now tied to EnergyConservationReq (the definition) by subsetting ([{'tying_element': 'ToasterDemo::EnergyConservationReq::c', 'field': 'subsets', 'requirement': 'ToasterDemo::EnergyConservationReq'}]), added by notebook 01 to close that gap -- not a claim that no other tie could exist by any conceivable mechanism, only that this one, real (tied_to_a_requirement=True), is closed.
AS-C06 (asserted_solution, Chapter 6): ResistanceCoil selected over a combustion alternative; engineering_conclusion=undetermined, argued from a domain premise, not a trade study.
AS-C08 (asserted_solution, Chapter 8): deliveredEnergyBoundedBySupply proved by Z3; engineering_conclusion=supported, but the proof is a hand-restated lemma, not a solver-checked reference to HeatGenerator's own efficiencyBounded/deliveredEnergy.
AI-C06 (asserted_inference, Chapter 6): the level-2 heat-generation branch's own stopping judgment; engineering_conclusion=undetermined, energyIn not wired to any producer, HeatingAssembly not composed into any Toaster candidate.
AC-C10 (asserted_context, Chapter 10): frames the energyConservationReq tie honestly -- the subsetting mechanism is spec-legitimate (SS7.21.2) and the requirement's own general motivation (energy conservation) is genuine, but its own need was identified retroactively, after Chapter 8's proof, specifically to close this chapter's own traceability gap; the tie is purely structural (Check B alone), deliberately not reinforced by any assert-satisfy claim -- confirmed by direct test to fail under model.verify_satisfaction() regardless of which candidate is bound, and, separately, confirmed by contrast that adding it back makes sysmlv2 verify --solve reduce to the identical 'undecided, indeterminate over unbound features' verdict every other requirement's own unbound required constraint already gets in this model -- a real check, but one that still resolves nothing, not the absence of a check -- so requirement_coverage()'s own covered=False for it is correct and expected, not a residual gap.
['Toaster::cycleTime remains a settable, underived attribute (unchanged since Chapter 2); this record does not assume it has been derived from anything.']
What supports the claim, and how (sufficiency): the two notebooks’ own outputs above, cited directly.
evidence_refs = [
"notebook 01's own requirement_coverage() output and tie-evidence search "
"(this chapter, reproduced above)",
"notebook 02's own three reconstructed ReviewRecords, each independently "
"validated and diffed field-for-field against its real original (this "
"chapter)",
"notebook 01's own AC-C10, cited above",
]
rationale = (
"heatGenerationReq is the strongest-traced requirement in this model: a real "
"positive claim and a real negative claim both exist, though its own 600 W "
"threshold is still a free-standing engineering figure, not derived from any "
"stated measure of effectiveness (AC-C06, cited by AI-C06). timely is the "
"weakest: a real functional intent with a real allocation and real physical "
"candidates, but zero positive verification, since cycleTime is still not "
"derived from anything. deliveredEnergyBoundedBySupply is this tutorial's "
"single strongest piece of formal evidence, proved by Z3 for every value its "
"unbound features admit. Notebook 01's own traceability graph found it tied "
"to no requirement at all under this tutorial's two narrow, "
"explicitly-named checks -- the inverse of the 'unjustified widget' pattern "
"Douglas's own traceability concern names -- and closed that gap directly: "
"energyConservationReq, added specifically to restate the property the "
"lemma proves as a stakeholder-facing requirement, is now tied to it by "
"subsetting from within the requirement's own body (Check B). Deliberately "
"absent is any assert-satisfy claim: AC-C10 and notebook 01's own negative "
"control both confirm, by direct test rather than argument alone, that "
"idiom would not do real evaluative work here. That the tie now exists, "
"structurally, is a separate fact from a real limitation on the proof's own "
"scope (AS-C08's own counterevidence already says so): the proof is of a "
"hand-restated companion lemma, not a solver-checked link to HeatGenerator's "
"own real elements, and closing the traceability gap does not strengthen "
"what was actually proved. It is also a separate fact from a real "
"limitation on the tie's own scope (AC-C10's own counterevidence already "
"says so): this requirement's own need was identified retroactively, not "
"before the evidence that motivated it, and the tie rests on structural "
"detection alone, with no independent solver-level re-verification. Taken "
"together, this is a partial, honestly-scoped basis for sign-off, not a "
"completed one."
)
print(rationale)heatGenerationReq is the strongest-traced requirement in this model: a real positive claim and a real negative claim both exist, though its own 600 W threshold is still a free-standing engineering figure, not derived from any stated measure of effectiveness (AC-C06, cited by AI-C06). timely is the weakest: a real functional intent with a real allocation and real physical candidates, but zero positive verification, since cycleTime is still not derived from anything. deliveredEnergyBoundedBySupply is this tutorial's single strongest piece of formal evidence, proved by Z3 for every value its unbound features admit. Notebook 01's own traceability graph found it tied to no requirement at all under this tutorial's two narrow, explicitly-named checks -- the inverse of the 'unjustified widget' pattern Douglas's own traceability concern names -- and closed that gap directly: energyConservationReq, added specifically to restate the property the lemma proves as a stakeholder-facing requirement, is now tied to it by subsetting from within the requirement's own body (Check B). Deliberately absent is any assert-satisfy claim: AC-C10 and notebook 01's own negative control both confirm, by direct test rather than argument alone, that idiom would not do real evaluative work here. That the tie now exists, structurally, is a separate fact from a real limitation on the proof's own scope (AS-C08's own counterevidence already says so): the proof is of a hand-restated companion lemma, not a solver-checked link to HeatGenerator's own real elements, and closing the traceability gap does not strengthen what was actually proved. It is also a separate fact from a real limitation on the tie's own scope (AC-C10's own counterevidence already says so): this requirement's own need was identified retroactively, not before the evidence that motivated it, and the tie rests on structural detection alone, with no independent solver-level re-verification. Taken together, this is a partial, honestly-scoped basis for sign-off, not a completed one.
What could be wrong, and what is still open (trustworthiness): named plainly, not folded into a tidier-sounding conclusion. The deliveredEnergyBoundedBySupply lemma named below is hand-restated, not solver-linked, because of two deferred solver gaps, DEFERRED.md D-030 and DEFERRED.md D-031.
counterevidence = (
"No physical realization of the toaster as a whole has been checked "
"end-to-end. ResistanceCoil's own mechanism selection rests on a domain "
"premise, not a trade study (AS-C06). HeatGenerator::energyIn is still not "
"wired to a producer, and HeatingAssembly is not composed into any Toaster "
"candidate (AI-C06). heatGenerationReq's own 600 W threshold is not derived "
"from any stated measure of effectiveness (AC-C06, cited by AI-C06). "
"Toaster::cycleTime remains unset from anything (unchanged since Chapter 2), "
"so timely's own coverage gap cannot be closed by more querying alone, only "
"by new modeling work. deliveredEnergyBoundedBySupply's Z3 proof is of a "
"hand-restated companion lemma, not a solver-checked reference to "
"HeatGenerator's own efficiencyBounded/deliveredEnergy (DEFERRED.md D-030, "
"D-031); tying it to energyConservationReq (notebook 01) closes the "
"traceability gap but does not strengthen the proof itself -- the tie and "
"the proof's own scope are two separate facts, honestly disclosed in "
"AC-C10 (notebook 01), not in the requirement's own doc comment alone. "
"AC-C10 also names its own open question directly: a requirement identified "
"after the evidence it is tied to, closing a gap that same analysis found, "
"is a real, honestly-named assurance deficit about circularity, not "
"resolved here."
)
residual_uncertainties = (
"Whether ResistanceCoil remains the right mechanism selection once a supply "
"and a control policy are modeled together (AS-C06's own open question). "
"Whether the restated deliveredEnergyBoundedBySupply lemma would still hold "
"if HeatGenerator's own efficiencyBounded or deliveredEnergy were edited "
"without also updating the restatement; nothing in this toolchain checks "
"that automatically (AS-C08's own residual). Whether cycleTime should ever "
"be derived, and from what, before timely can be positively checked at all, "
"and, if it were, whether nominal would actually satisfy it, which no "
"evidence in this model addresses either way. Whether a requirement whose "
"own need was identified after its own evidence should ever be accepted "
"without qualification, or whether this tutorial should adopt a stricter "
"rule (AC-C10's own open question). None of this is decided here: it is "
"exactly the kind of judgment an accountable engineer, not this tutorial, "
"has to exercise before actually shipping this design."
)
print(counterevidence)
print()
print(residual_uncertainties)
No physical realization of the toaster as a whole has been checked end-to-end. ResistanceCoil's own mechanism selection rests on a domain premise, not a trade study (AS-C06). HeatGenerator::energyIn is still not wired to a producer, and HeatingAssembly is not composed into any Toaster candidate (AI-C06). heatGenerationReq's own 600 W threshold is not derived from any stated measure of effectiveness (AC-C06, cited by AI-C06). Toaster::cycleTime remains unset from anything (unchanged since Chapter 2), so timely's own coverage gap cannot be closed by more querying alone, only by new modeling work. deliveredEnergyBoundedBySupply's Z3 proof is of a hand-restated companion lemma, not a solver-checked reference to HeatGenerator's own efficiencyBounded/deliveredEnergy (DEFERRED.md D-030, D-031); tying it to energyConservationReq (notebook 01) closes the traceability gap but does not strengthen the proof itself -- the tie and the proof's own scope are two separate facts, honestly disclosed in AC-C10 (notebook 01), not in the requirement's own doc comment alone. AC-C10 also names its own open question directly: a requirement identified after the evidence it is tied to, closing a gap that same analysis found, is a real, honestly-named assurance deficit about circularity, not resolved here.
Whether ResistanceCoil remains the right mechanism selection once a supply and a control policy are modeled together (AS-C06's own open question). Whether the restated deliveredEnergyBoundedBySupply lemma would still hold if HeatGenerator's own efficiencyBounded or deliveredEnergy were edited without also updating the restatement; nothing in this toolchain checks that automatically (AS-C08's own residual). Whether cycleTime should ever be derived, and from what, before timely can be positively checked at all, and, if it were, whether nominal would actually satisfy it, which no evidence in this model addresses either way. Whether a requirement whose own need was identified after its own evidence should ever be accepted without qualification, or whether this tutorial should adopt a stricter rule (AC-C10's own open question). None of this is decided here: it is exactly the kind of judgment an accountable engineer, not this tutorial, has to exercise before actually shipping this design.
Assembling the record from the named parts above. kind="asserted_inference" is the deliberate choice here, not asserted_solution: this record’s own premises are literally child claims (the ledger’s three records, plus AC-C10, plus notebook 01’s own coverage and tie findings) supporting a parent synthesis, exactly Hawkins’ own “child claims supporting a parent” idea (SS3.1), not new evidence of its own.
from toaster.query import get_review_record_refs
signoff = ReviewRecord(
identifier="AI-C10",
kind="asserted_inference",
claim=claim,
model_ref=model_ref,
content_hash=hash_content(source),
scope=scope,
criteria=criteria,
premises=premises,
assumption_refs=assumption_refs,
evidence_refs=evidence_refs,
rationale=rationale,
counterevidence=counterevidence,
residual_uncertainties=residual_uncertainties,
disposition="pending",
dependency_freshness="current",
engineering_conclusion="undetermined",
record_kind="worked_example",
)
errors = validate_record(signoff, model=model)
tag = next((t for t in get_review_record_refs(model) if t["identifier"] == signoff.identifier), None)
print(f"Model tag: {tag}")
print(f"Validation errors: {errors}")
print(f"identifier={signoff.identifier!r} kind={signoff.kind!r}")
print(f"disposition={signoff.disposition!r} record_kind={signoff.record_kind!r}")
print(f"engineering_conclusion={signoff.engineering_conclusion!r}")
assert errors == []
assert not any("subject_ref" in e for e in errors)
assert tag is None
assert signoff.disposition == "pending"
assert signoff.record_kind == "worked_example"
conn.close()
Model tag: None
Validation errors: []
identifier='AI-C10' kind='asserted_inference'
disposition='pending' record_kind='worked_example'
engineering_conclusion='undetermined'
AI-C10 carries no subject_ref and gets no ReviewRecordRef tag: the exemption validate_record() grants is this tutorial’s own rule for the pure cross-record synthesis case -- an asserted_inference whose own premises are non-empty may leave subject_ref unset -- and AI-C10’s own premises, printed above, really are non-empty: five real findings, not a placeholder list. Model tag: None and zero subject_ref-related validation errors, both confirmed directly above against the real loaded model, are what that exemption actually looks like when exercised for real, not merely argued. AI-C10 is not the only record the rule could apply to -- AI-C10-DRAFT above and AI-C04 (Chapter 4) both have non-empty premises too, and the rule would exempt either the same way -- it is simply the one record in this chapter that actually uses the exemption rather than carrying a real anchor anyway.
engineering_conclusion stays undetermined, not supported: one of the model’s two original requirements is genuinely covered, one is not, and although the model’s own strongest proof is now tied to its own new requirement (energyConservationReq, closing the gap notebook 01 found, structurally rather than by any point check), that tie settles neither timely’s own uncovered state nor anything else this record’s own residual still names, so no single word honestly describes the model as a whole except the word that admits the mixture. Say plainly what this record is, and is not: it is a synthesis of two real, already-verified inputs into one honest, bounded statement of what is established, what is not, and what residual judgment remains. It is not sign-off. A completed traceability graph and judgment ledger tell an engineer what they are working with; deciding whether that is enough to actually proceed, given the real residual uncertainties named above, is a human, accountable act this tutorial can show the inputs to but cannot perform on the learner’s behalf.
AGENTS.md’s own account of emergence names what a real sign-off actually has to weigh, beyond anything this record states: “strong emergence (unanticipated; seen only in integration, test or operation) belongs to no layer. It is what sign-off judges.” This chapter’s own synthesis, however honestly built and however carefully bounded, cannot anticipate strong emergence by construction: it is a map of what has already been checked and what has not, not a forecast of what integration or operation might still reveal. It is exactly the kind of artifact a real engineer would weigh against that residual, unanticipated risk before deciding to proceed, not a substitute for weighing it. A traceable, honestly-scoped case makes that judgment easier to exercise well; it does not make the judgment itself unnecessary.
Three notebooks, one arc: a real traceability graph that traces two requirements very differently, finds the model’s own strongest proof tied to no requirement at all, and closes that gap directly; a judgment ledger over three real records, two of them still undetermined, plus AC-C10’s own honest framing of the new tie; and a synthesis record that states honestly what all of that does, and does not, establish, with disposition="pending" like every other record this tutorial has built.
Try the chapter exercise in exercises/ch10/exercise.ipynb: it asks you to build this same traceability graph, judgment ledger and sign-off synthesis over your own coffee-maker model.