%22%22%22%23%20ADCS%20Lifecycle%20Demo%3A%20Bidirectional%20Requirements%20Traceability%0A%0AA%20walkthrough%20of%20satellite%20attitude%20control%20system%20design%20%E2%80%94%20from%20receiving%0Arequirements%20through%20symbolic%20analysis%2C%20numerical%20simulation%2C%20evidence%0Abinding%2C%20human%20attestation%2C%20and%20audit.%0A%22%22%22%0A%0Aimport%20marimo%0A%0A__generated_with%20%3D%20%220.22.5%22%0Aapp%20%3D%20marimo.App(width%3D%22medium%22)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20%23%20ADCS%20Lifecycle%20Demo%0A%0A%20%20%20%20%23%23%20Bidirectional%20Requirements%20Traceability%20with%20Reproducible%20Evidence%0A%0A%20%20%20%20This%20notebook%20walks%20through%20the%20complete%20lifecycle%20of%20verifying%20an%0A%20%20%20%20**Attitude%20Determination%20and%20Control%20System%20(ADCS)**%20for%20a%20geostationary%0A%20%20%20%20communications%20satellite.%0A%0A%20%20%20%20We%20follow%20the%20perspective%20of%20the%20**controls%20engineering%20team**%20%E2%80%94%20one%0A%20%20%20%20disciplinary%20team%20within%20a%20larger%20satellite%20design%20program.%20Our%20job%20is%0A%20%20%20%20to%20demonstrate%20that%20the%20ADCS%20meets%20its%20requirements%2C%20with%20evidence%20that%0A%20%20%20%20any%20auditor%20can%20interrogate%20and%20reproduce.%0A%0A%20%20%20%20%23%23%23%20Core%20Principle%0A%0A%20%20%20%20%3E%20**Evidence%20does%20not%20verify%20requirements%3B%20evidence%20supports%20a%20human%0A%20%20%20%20%3E%20judgment%20that%20requirements%20are%20satisfied.**%0A%0A%20%20%20%20Models%20are%20imperfect%20representations%20of%20physical%20systems.%20Symbolic%20proofs%0A%20%20%20%20and%20simulation%20results%20are%20claims%20true%20*within%20the%20model*.%20The%20engineer%0A%20%20%20%20judges%20model%20adequacy%20and%20evidence%20sufficiency.%20Only%20human%20attestation%0A%20%20%20%20connects%20evidence%20to%20requirement%20satisfaction.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Prologue%3A%20The%20Integration%20Ontology%0A%0A%20%20%20%20Before%20we%20write%20a%20single%20line%20of%20analysis%20code%2C%20we%20have%20an%0A%20%20%20%20epistemological%20question%20to%20settle%3A%20**what%20counts%20as%20a%20satisfactory%0A%20%20%20%20requirement%3F**%0A%0A%20%20%20%20A%20naive%20demo%20would%20invent%20terms%20%E2%80%94%20%60rtm%3AmodelAdequacy%60%2C%20a%20custom%0A%20%20%20%20%22satisfaction%22%20predicate%2C%20a%20bespoke%20evidence%20vocabulary.%20This%20demo%0A%20%20%20%20deliberately%20does%20the%20opposite.%20The%20%60rtm%3A%60%20namespace%20introduces%20**no%0A%20%20%20%20novel%20epistemic%20vocabulary.**%20It%20is%20a%20thin%20*integration%20ontology*%20over%0A%20%20%20%20established%20standards%3A%0A%0A%20%20%20%20%7C%20Layer%20%20%20%20%20%20%20%20%7C%20Vocabulary%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%7C%20Role%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%7C%0A%20%20%20%20%7C%20------------%20%7C%20------------------------------------%20%7C%20--------------------------------------------------------%20%7C%0A%20%20%20%20%7C%20W3C%20%2F%20IETF%20%20%20%7C%20%60prov%3A%60%2C%20%60dcterms%3A%60%2C%20%60earl%3A%60%2C%20%60sh%3A%60%20%20%7C%20Provenance%20%2B%20assertion%20%2B%20outcome%20%2B%20SHACL%20closure%20%20%20%20%20%20%20%20%20%7C%0A%20%20%20%20%7C%20OMG%20%2F%20SysML%20%20%7C%20%60sysml%3A%60%20%E2%86%94%20%60omg-sysml%3A%60%20%20%20%20%20%20%20%20%20%20%20%20%20%20%7C%20Structural%20model%20(aliased%20to%20openCAESAR%20OWL%20rendering)%20%20%20%7C%0A%20%20%20%20%7C%20Community%20%20%20%20%7C%20%60gsn%3A%60%2C%20%60p-plan%3A%60%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%7C%20Assurance%20argument%20structure%20%2B%20declarative%20process%20model%20%7C%0A%20%20%20%20%7C%20Tool%20interop%20%7C%20%60oslc_rm%3A%60%2C%20%60oslc_qm%3A%60%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%7C%20Aliases%20for%20DOORS%20Next%20%2F%20Jama%20%2F%20RQM%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%7C%0A%0A%20%20%20%20The%20adequacy%2Fsufficiency%20split%20is%20**not%20novel**%20either%20%E2%80%94%20it's%20the%0A%20%20%20%20canonical%20Hawkins%E2%80%93Habli%20Assurance%20Claim%20Point%20categorization.%0A%20%20%20%20%22Adequacy%22%20is%20a%20%60gsn%3AAssumption%60%3B%20%22sufficiency%22%20is%20a%0A%20%20%20%20%60gsn%3AJustification%60.%20Both%20attach%20to%20the%20attestation%20via%0A%20%20%20%20%60gsn%3AinContextOf%60.%20The%20text%20content%20lives%20on%20those%20GSN%20nodes%20in%0A%20%20%20%20%60gsn%3Astatement%60.%0A%0A%20%20%20%20The%20pipeline%20runs%20this%20assembly%20as%20its%20first%20act%20%E2%80%94%20narrating%20which%0A%20%20%20%20upstream%20ontologies%20were%20imported%2C%20how%20many%20terms%20we%20reference%2C%20and%0A%20%20%20%20what%20closure%20rules%20will%20be%20enforced%20downstream.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20import%20json%20as%20_json%0A%20%20%20%20from%20pathlib%20import%20Path%20as%20_Path%0A%0A%20%20%20%20_manifest%20%3D%20_json.loads(_Path(%22ontology%2Fassembly_manifest.json%22).read_text())%0A%0A%20%20%20%20_import_rows%20%3D%20%5B%5D%0A%20%20%20%20for%20_name%20in%20sorted(_manifest%5B%22imports%22%5D)%3A%0A%20%20%20%20%20%20%20%20_info%20%3D%20_manifest%5B%22imports%22%5D%5B_name%5D%0A%20%20%20%20%20%20%20%20_import_rows.append(%0A%20%20%20%20%20%20%20%20%20%20%20%20f%22%7C%20%7B_name%7D%20%7C%20%7B_info%5B'total_triples'%5D%3A%3E5%7D%20%7C%20%7B_info%5B'referenced_count'%5D%7D%20%7C%22%0A%20%20%20%20%20%20%20%20)%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Assembly%20manifest%20(data-driven%2C%20not%20hand-written)%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22Built%20%60%7B_manifest%5B'build_time'%5D%7D%60%20from%20%60ontology%2Frtm-edit.ttl%60.%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Upstream%20%7C%20Triples%20%7C%20TBox%20refs%20in%20%60rtm-edit.ttl%60%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C---%7C---%3A%7C---%3A%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%2B%20%22%5Cn%22.join(_import_rows)%20%2B%20%22%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22-%20**SysMLv2%20equivalence%20axioms**%20(sysml%3A%20%E2%86%94%20omg-sysml%3A)%3A%20%22%0A%20%20%20%20%20%20%20%20f%22%7B_manifest%5B'artifact'%5D%5B'equivalence_axioms'%5D%7D%5Cn%22%0A%20%20%20%20%20%20%20%20f%22-%20**Local%20rtm%3A%20integration%20glue%3A**%20%22%0A%20%20%20%20%20%20%20%20f%22%7B_manifest%5B'artifact'%5D%5B'subclass_axioms'%5D%7D%20subclass%20%2B%20%22%0A%20%20%20%20%20%20%20%20f%22%7B_manifest%5B'artifact'%5D%5B'subproperty_axioms'%5D%7D%20subproperty%20axioms%20%22%0A%20%20%20%20%20%20%20%20f%22(no%20novel%20epistemic%20terms)%5Cn%22%0A%20%20%20%20%20%20%20%20f%22-%20**Artifact%20SHA-256%3A**%20%60%7B_manifest%5B'artifact'%5D%5B'sha256'%5D%5B%3A24%5D%7D...%60%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**About%20the%20third%20column.**%20*TBox%20refs*%20counts%20how%20many%20distinct%20%22%0A%20%20%20%20%20%20%20%20%22terms%20from%20each%20upstream%20namespace%20appear%20in%20our%20integration%20%22%0A%20%20%20%20%20%20%20%20%22ontology%20source%20%60rtm-edit.ttl%60%20%E2%80%94%20i.e.%20how%20often%20that%20vocabulary%20%22%0A%20%20%20%20%20%20%20%20%22is%20used%20as%20the%20target%20of%20a%20%60rdfs%3AsubClassOf%60%20%2F%20%60rdfs%3AsubPropertyOf%60%20%22%0A%20%20%20%20%20%20%20%20%22alignment%20axiom.%20**P-PLAN%20reads%200**%20because%20P-PLAN%20is%20used%20at%20the%20%22%0A%20%20%20%20%20%20%20%20%22*instance%20%2F%20runtime*%20layer%20rather%20than%20the%20TBox%20alignment%20layer%3A%20%22%0A%20%20%20%20%20%20%20%20%22the%20plan%20definition%20lives%20in%20%60pipeline%2Fplan.ttl%60%20(instance%20data%2C%20%22%0A%20%20%20%20%20%20%20%20%2210%20%60p-plan%3AStep%60%20instances)%20and%20per-stage%20%60p-plan%3AActivity%60%20%22%0A%20%20%20%20%20%20%20%20%22triples%20are%20emitted%20at%20runtime%20by%20%60traceability.plan_execution%60.%20%22%0A%20%20%20%20%20%20%20%20%22Vendoring%20an%20upstream%20is%20not%20the%20same%20as%20subclassing%20it.%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22The%20manifest%20is%20the%20build-step%20provenance%20record.%20Stage%200%20of%20the%20%22%0A%20%20%20%20%20%20%20%20%22pipeline%20verifies%20that%20%60rtm.ttl%60%20still%20hashes%20to%20this%20manifest%20%22%0A%20%20%20%20%20%20%20%20%22value%20%E2%80%94%20drift%20between%20the%20source%20%60rtm-edit.ttl%60%20and%20the%20committed%20%22%0A%20%20%20%20%20%20%20%20%22artifact%20fails%20the%20pipeline%20with%20a%20clear%20remediation%20hint.%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20%23%23%23%20Named-graph%20quadstore%20layout%0A%0A%20%20%20%20The%20runtime%20holds%20the%20RTM%20as%20an%20%60rdflib.Dataset%60%20(a%20quadstore)%20with%0A%20%20%20%20one%20named%20graph%20per%20content%20layer%20%E2%80%94%20sized%20to%20match%20how%20Flexo%20MMS%0A%20%20%20%20partitions%20projects%2Fbranches.%20SPARQL%20queries%20use%0A%20%20%20%20%60Dataset(default_union%3DTrue)%60%20so%20existing%20queries%20match%20across%20the%0A%20%20%20%20union%20without%20%60GRAPH%60%20clauses.%0A%0A%20%20%20%20%60%60%60text%0A%20%20%20%20%3Crtm%3Aontology%3E%20%20%20%20%20%20%20%20TBox%20%2B%20shapes%20%2B%20individuals%0A%20%20%20%20%3Crtm%3Aplan%3E%20%20%20%20%20%20%20%20%20%20%20%20P-PLAN%20process%20model%20(one%20Step%20per%20pipeline%20stage)%0A%20%20%20%20%3Cadcs%3Astructural%3E%20%20%20%20%20SysMLv2%20instance%20data%0A%20%20%20%20%3Cadcs%3Acontext%3E%20%20%20%20%20%20%20%20Stable%20gsn%3AContext%20%2F%20gsn%3AAssumption%20individuals%0A%20%20%20%20%3Cadcs%3Aevidence%3E%20%20%20%20%20%20%20rtm%3AEvidence%20artifacts%0A%20%20%20%20%3Cadcs%3Aattestations%3E%20%20%20rtm%3AAttestation%20events%0A%20%20%20%20%3Cadcs%3Aplan-execution%3E%20p-plan%3AActivity%20instances%20(one%20per%20stage)%0A%20%20%20%20%3Cadcs%3Aaudit%3E%20%20%20%20%20%20%20%20%20%20Forward%2Fbackward%2Fbidirectional%20audit%20summary%0A%20%20%20%20%60%60%60%0A%0A%20%20%20%20Stage%207%20persists%20the%20Dataset%20to%20disk%20(%60output%2Frtm.%7Bttl%2Ctrig%7D%60)%20or%20to%20a%0A%20%20%20%20real%20quadstore%20(Flexo%20MMS%20%2F%20Apache%20Jena%20Fuseki)%20via%20pluggable%0A%20%20%20%20backends.%20Either%20way%2C%20every%20named%20graph%20round-trips%20cleanly.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%201%3A%20The%20Assignment%0A%0A%20%20%20%20You%20are%20Dr.%20Michael%20Zargham%2C%20lead%20controls%20engineer%20on%20the%20GeoSat%0A%20%20%20%20communications%20satellite%20program.%20Systems%20engineering%20has%20allocated%0A%20%20%20%20four%20requirements%20to%20your%20ADCS%20subsystem%2C%20each%20derived%20from%0A%20%20%20%20satellite-level%20requirements.%0A%0A%20%20%20%20Your%20team%20owns%20the%20ADCS%20%E2%80%94%20reaction%20wheels%2C%20star%20tracker%2C%20IMU%2C%20and%20the%0A%20%20%20%20PD%20attitude%20controller.%20You%20consume%20interface%20parameters%20(mass%2C%20orbit%2C%0A%20%20%20%20panel%20geometry)%20from%20other%20teams%20but%20don't%20control%20them.%0A%0A%20%20%20%20%60%60%60%0A%20%20%20%20Satellite%20(system-of-interest)%0A%20%20%20%20%E2%94%9C%E2%94%80%E2%94%80%20ADCS%20%20%20%20%20%20%20%20%20%20%20%E2%86%90%20YOUR%20SCOPE%0A%20%20%20%20%E2%94%9C%E2%94%80%E2%94%80%20Power%20%20%20%20%20%20%20%20%20%20%E2%86%90%20interface%3A%20power%20budget%0A%20%20%20%20%E2%94%9C%E2%94%80%E2%94%80%20Communications%20%E2%86%90%20interface%3A%20antenna%20pointing%0A%20%20%20%20%E2%94%9C%E2%94%80%E2%94%80%20Thermal%20%20%20%20%20%20%20%20%E2%86%90%20interface%3A%20wheel%20heat%20dissipation%0A%20%20%20%20%E2%94%94%E2%94%80%E2%94%80%20Structure%20%20%20%20%20%20%E2%86%90%20interface%3A%20mass%20properties%0A%20%20%20%20%60%60%60%0A%0A%20%20%20%20Let's%20load%20the%20structural%20model%20and%20see%20what%20we're%20working%20with.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_()%3A%0A%20%20%20%20import%20sys%0A%20%20%20%20sys.path.insert(0%2C%20%22.%22)%0A%0A%20%20%20%20from%20rdflib%20import%20Graph%0A%20%20%20%20from%20ontology.prefixes%20import%20bind_prefixes%2C%20SYSML%2C%20RTM%2C%20ADCS%2C%20SAT%2C%20PROV%0A%20%20%20%20from%20traceability.queries%20import%20query_to_dicts%0A%0A%20%20%20%20return%20(query_to_dicts%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_()%3A%0A%20%20%20%20from%20analysis.load_params%20import%20load_structural_graph%2C%20load_params%0A%0A%20%20%20%20struct_graph%20%3D%20load_structural_graph()%0A%20%20%20%20params%20%3D%20load_params(struct_graph)%0A%20%20%20%20return%20params%2C%20struct_graph%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20params)%3A%0A%20%20%20%20_param_rows%20%3D%20%22%5Cn%22.join(%0A%20%20%20%20%20%20%20%20f%22%7C%20%7Bk%7D%20%7C%20%7Bv%3A.6g%7D%20%7C%22%20for%20k%2C%20v%20in%20sorted(params.items())%0A%20%20%20%20)%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Structural%20Parameters%20(from%20RDF%20via%20SPARQL)%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22All%20parameters%20flow%20from%20the%20SysMLv2%20structural%20model%20%E2%80%94%20nothing%20is%20%22%0A%20%20%20%20%20%20%20%20%22hardcoded.%20If%20systems%20engineering%20updates%20the%20satellite%20mass%2C%20our%20%22%0A%20%20%20%20%20%20%20%20%22entire%20analysis%20chain%20re-derives%20from%20the%20new%20value.%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Parameter%20%7C%20Value%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C-----------%7C-------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7B_param_rows%7D%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20query_to_dicts%2C%20struct_graph)%3A%0A%20%20%20%20_req_query%20%3D%20%22%22%22%0A%20%20%20%20SELECT%20%3Fname%20%3Ftext%20WHERE%20%7B%0A%20%20%20%20%20%20%20%20%3Freq%20a%20sysml%3ARequirementDefinition%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20sysml%3AdeclaredName%20%3Fname%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20sysml%3Atext%20%3Ftext%20.%0A%20%20%20%20%20%20%20%20FILTER(STRSTARTS(%3Fname%2C%20%22REQ-%22))%0A%20%20%20%20%7D%0A%20%20%20%20ORDER%20BY%20%3Fname%0A%20%20%20%20%22%22%22%0A%20%20%20%20_reqs%20%3D%20query_to_dicts(struct_graph%2C%20_req_query)%0A%0A%20%20%20%20_deriv_query%20%3D%20%22%22%22%0A%20%20%20%20SELECT%20%3Fchild%20%3Fparent%20WHERE%20%7B%0A%20%20%20%20%20%20%20%20%3Fc%20sysml%3AdeclaredName%20%3Fchild%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20rtm%3AderivedFrom%20%3Fp%20.%0A%20%20%20%20%20%20%20%20%3Fp%20sysml%3AdeclaredName%20%3Fparent%20.%0A%20%20%20%20%7D%0A%20%20%20%20ORDER%20BY%20%3Fchild%0A%20%20%20%20%22%22%22%0A%20%20%20%20_derivs%20%3D%20query_to_dicts(struct_graph%2C%20_deriv_query)%0A%20%20%20%20_deriv_map%20%3D%20%7Br%5B%22child%22%5D%3A%20r%5B%22parent%22%5D%20for%20r%20in%20_derivs%7D%0A%0A%20%20%20%20_alloc_query%20%3D%20%22%22%22%0A%20%20%20%20SELECT%20%3FreqName%20%3FelementName%20WHERE%20%7B%0A%20%20%20%20%20%20%20%20%3Freq%20sysml%3AdeclaredName%20%3FreqName%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20sysml%3AownedRelationship%20%3Frel%20.%0A%20%20%20%20%20%20%20%20%3Frel%20a%20sysml%3ASatisfyRequirementUsage%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20sysml%3AsatisfyingElement%20%3Fel%20.%0A%20%20%20%20%20%20%20%20%3Fel%20sysml%3AdeclaredName%20%3FelementName%20.%0A%20%20%20%20%20%20%20%20FILTER(STRSTARTS(%3FreqName%2C%20%22REQ-%22))%0A%20%20%20%20%7D%0A%20%20%20%20ORDER%20BY%20%3FreqName%20%3FelementName%0A%20%20%20%20%22%22%22%0A%20%20%20%20_allocs%20%3D%20query_to_dicts(struct_graph%2C%20_alloc_query)%0A%0A%20%20%20%20_alloc_map%20%3D%20%7B%7D%0A%20%20%20%20for%20_a%20in%20_allocs%3A%0A%20%20%20%20%20%20%20%20_alloc_map.setdefault(_a%5B%22reqName%22%5D%2C%20%5B%5D).append(_a%5B%22elementName%22%5D)%0A%0A%20%20%20%20_req_rows%20%3D%20%5B%5D%0A%20%20%20%20for%20_r%20in%20_reqs%3A%0A%20%20%20%20%20%20%20%20_name%20%3D%20_r%5B%22name%22%5D%0A%20%20%20%20%20%20%20%20_text%20%3D%20_r%5B%22text%22%5D.strip().replace(%22%5Cn%22%2C%20%22%20%22)%5B%3A80%5D%0A%20%20%20%20%20%20%20%20_parent%20%3D%20_deriv_map.get(_name%2C%20%22%E2%80%94%22)%0A%20%20%20%20%20%20%20%20_elements%20%3D%20%22%2C%20%22.join(_alloc_map.get(_name%2C%20%5B%5D))%0A%20%20%20%20%20%20%20%20_req_rows.append(f%22%7C%20%7B_name%7D%20%7C%20%7B_text%7D...%20%7C%20%7B_parent%7D%20%7C%20%7B_elements%7D%20%7C%22)%0A%0A%20%20%20%20_req_table%20%3D%20%22%5Cn%22.join(_req_rows)%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20ADCS%20Requirements%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22Four%20requirements%20allocated%20to%20us%2C%20each%20derived%20from%20a%20satellite-level%20%22%0A%20%20%20%20%20%20%20%20%22parent%20requirement%20and%20satisfied%20by%20specific%20design%20elements%3A%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20ID%20%7C%20Requirement%20%7C%20Derived%20From%20%7C%20Satisfied%20By%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C----%7C------------%7C-------------%7C-------------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7B_req_table%7D%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%202%3A%20Symbolic%20Analysis%0A%0A%20%20%20%20Before%20running%20any%20simulation%2C%20we%20derive%20formal%20results%20symbolically%0A%20%20%20%20using%20SymPy.%20Every%20quantity%20is%20computed%20from%20the%20structural%20parameters%20%E2%80%94%0A%20%20%20%20the%20inertia%20tensor%20via%20parallel%20axis%20theorem%2C%20eigenvalues%20for%20stability%0A%20%20%20%20analysis%2C%20and%20bounds%20for%20pointing%20error%20and%20wheel%20momentum.%0A%0A%20%20%20%20These%20are%20claims%20true%20*within%20our%20model*.%20Whether%20the%20model%20adequately%0A%20%20%20%20represents%20the%20physical%20satellite%20is%20a%20judgment%20we'll%20make%20during%0A%20%20%20%20attestation.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(params)%3A%0A%20%20%20%20from%20analysis.symbolic%20import%20(%0A%20%20%20%20%20%20%20%20run_symbolic_analysis%2C%0A%20%20%20%20%20%20%20%20build_inertia_tensor_symbolic%2C%0A%20%20%20%20%20%20%20%20evaluate_inertia%2C%0A%20%20%20%20%20%20%20%20stability_margins%2C%0A%20%20%20%20)%0A%0A%20%20%20%20sym_result%20%3D%20run_symbolic_analysis(params)%0A%20%20%20%20return%20(sym_result%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20sym_result)%3A%0A%20%20%20%20_Ixx%2C%20_Iyy%2C%20_Izz%20%3D%20sym_result.inertia%0A%20%20%20%20_margins%20%3D%20sym_result.stability_margins%0A%0A%20%20%20%20mo.md(f%22%22%22%0A%20%20%20%20%23%23%23%20Composite%20Inertia%20Tensor%0A%0A%20%20%20%20Derived%20via%20parallel%20axis%20theorem%20(bus%20%2B%202%20solar%20panels%20%2B%20antenna)%3A%0A%0A%20%20%20%20%7C%20Axis%20%7C%20Inertia%20(kg-m%5E2)%20%7C%20Dominant%20contributor%20%7C%0A%20%20%20%20%7C------%7C-----------------%7C---------------------%7C%0A%20%20%20%20%7C%20Ixx%20%20%7C%20%7B_Ixx%3A.1f%7D%20%7C%20Solar%20panels%20(offset%20along%20Y)%20%7C%0A%20%20%20%20%7C%20Iyy%20%20%7C%20%7B_Iyy%3A.1f%7D%20%7C%20Bus%20(panels%20add%20little%20on%20this%20axis)%20%7C%0A%20%20%20%20%7C%20Izz%20%20%7C%20%7B_Izz%3A.1f%7D%20%7C%20Solar%20panels%20(offset%20along%20Y)%20%7C%0A%0A%20%20%20%20The%20panels%20dominate%20Ixx%20and%20Izz%20because%20their%20center%20of%20mass%20is%20far%0A%20%20%20%20from%20the%20satellite%20center%20%E2%80%94%20the%20parallel%20axis%20term%20grows%20as%20distance%0A%20%20%20%20squared.%0A%0A%20%20%20%20%23%23%23%20Stability%20Margins%20(REQ-003)%0A%0A%20%20%20%20Closed-loop%20eigenvalues%20for%20each%20axis%20(PD%20controller%2C%20linearized)%3A%0A%0A%20%20%20%20%7C%20Axis%20%7C%20Re(lambda)%20%7C%20Margin%20vs%20-0.010%20%7C%0A%20%20%20%20%7C------%7C-----------%7C-----------------%7C%0A%20%20%20%20%7C%20X%20%7C%20%7B_margins%5B'x'%5D%3A.4f%7D%20rad%2Fs%20%7C%20%7B'PASS'%20if%20_margins%5B'x'%5D%20%3C%3D%20-0.010%20else%20'MARGINAL'%7D%20%7C%0A%20%20%20%20%7C%20Y%20%7C%20%7B_margins%5B'y'%5D%3A.4f%7D%20rad%2Fs%20%7C%20%7B'PASS'%20if%20_margins%5B'y'%5D%20%3C%3D%20-0.010%20else%20'MARGINAL'%7D%20%7C%0A%20%20%20%20%7C%20Z%20%7C%20%7B_margins%5B'z'%5D%3A.4f%7D%20rad%2Fs%20%7C%20%7B'PASS'%20if%20_margins%5B'z'%5D%20%3C%3D%20-0.010%20else%20'MARGINAL'%7D%20%7C%0A%0A%20%20%20%20All%20axes%20satisfy%20REQ-003%20(Re(lambda)%20%3C%3D%20-0.010%20rad%2Fs).%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20sym_result)%3A%0A%20%20%20%20_pb%20%3D%20sym_result.pointing_budget%0A%20%20%20%20_gg%20%3D%20sym_result.gravity_gradient%0A%20%20%20%20_wm%20%3D%20sym_result.wheel_momentum%0A%0A%20%20%20%20mo.md(f%22%22%22%0A%20%20%20%20%23%23%23%20Pointing%20Budget%20(REQ-001)%0A%0A%20%20%20%20%7C%20Metric%20%7C%20Value%20%7C%0A%20%20%20%20%7C--------%7C-------%7C%0A%20%20%20%20%7C%20Steady-state%20error%20(gravity%20gradient)%20%7C%20%7B_pb%5B'theta_ss_deg'%5D%3A.6f%7D%20deg%20%7C%0A%20%20%20%20%7C%20Star%20tracker%20noise%20floor%20%7C%20%7B_pb%5B'st_floor_deg'%5D%3A.6f%7D%20deg%20%7C%0A%20%20%20%20%7C%20Settling%20time%20(4%2F%7CRe(lambda)%7C)%20%7C%20%7B_pb%5B'settling_time_s'%5D%3A.1f%7D%20s%20%7C%0A%0A%20%20%20%20The%20steady-state%20pointing%20error%20is%20well%20below%200.1%20deg.%20However%2C%20the%0A%20%20%20%20**settling%20time%20is%20%7B_pb%5B'settling_time_s'%5D%3A.0f%7Ds**%20%E2%80%94%20exceeding%20the%20120s%20target.%0A%20%20%20%20This%20is%20a%20real%20finding%20that%20the%20engineer%20must%20address%20during%20attestation.%0A%0A%20%20%20%20%23%23%23%20Gravity%20Gradient%20(REQ-004)%0A%0A%20%20%20%20%7C%20Metric%20%7C%20Value%20%7C%0A%20%20%20%20%7C--------%7C-------%7C%0A%20%20%20%20%7C%20tau_gg_x%20%7C%20%7B_gg%5B'tau_gg_x'%5D%3A.2e%7D%20N.m%20%7C%0A%20%20%20%20%7C%20tau_gg_y%20%7C%20%7B_gg%5B'tau_gg_y'%5D%3A.2e%7D%20N.m%20%7C%0A%20%20%20%20%7C%20Actuator%20capacity%20%7C%20%7B_gg%5B'tau_max'%5D%7D%20N.m%20%7C%0A%0A%20%20%20%20Gravity%20gradient%20torques%20at%20GEO%20are%20**orders%20of%20magnitude**%20below%0A%20%20%20%20actuator%20capacity.%0A%0A%20%20%20%20%23%23%23%20Wheel%20Momentum%20(REQ-002)%0A%0A%20%20%20%20%7C%20Metric%20%7C%20Value%20%7C%0A%20%20%20%20%7C--------%7C-------%7C%0A%20%20%20%20%7C%20Peak%20momentum%20(10%20deg%20slew)%20%7C%20%7B_wm%5B'h_peak'%5D%3A.3f%7D%20N.m.s%20%7C%0A%20%20%20%20%7C%20Rated%20capacity%20%7C%20%7B_wm%5B'h_max'%5D%7D%20N.m.s%20%7C%0A%20%20%20%20%7C%20Margin%20%7C%20%7B_wm%5B'margin'%5D%3A.3f%7D%20N.m.s%20%7C%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20%23%23%23%20Formal%20Proofs%0A%0A%20%20%20%20Each%20requirement%20gets%20a%20ProofScript%20%E2%80%94%20a%20chain%20of%20SymPy%20lemmas%2C%20each%0A%20%20%20%20independently%20re-verifiable.%20The%20proof%20is%20bound%20to%20the%20structural%20model%0A%20%20%20%20via%20content%20hash%3A%20if%20the%20model%20changes%2C%20the%20proof%20hash%20changes%2C%20alerting%0A%20%20%20%20auditors%20to%20re-verify.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(struct_graph)%3A%0A%20%20%20%20from%20evidence.hashing%20import%20hash_structural_model%2C%20hash_proof%0A%20%20%20%20from%20analysis.build_proofs%20import%20build_all_proofs%0A%20%20%20%20from%20analysis.proof_scripts%20import%20verify_proof%2C%20ProofStatus%0A%0A%20%20%20%20model_hash%20%3D%20hash_structural_model(struct_graph)%0A%20%20%20%20proofs%20%3D%20build_all_proofs(model_hash)%0A%0A%20%20%20%20proof_results%20%3D%20%7B%7D%0A%20%20%20%20for%20_req_id%2C%20_script%20in%20proofs.items()%3A%0A%20%20%20%20%20%20%20%20_result%20%3D%20verify_proof(_script%2C%20model_hash)%0A%20%20%20%20%20%20%20%20proof_results%5B_req_id%5D%20%3D%20_result%0A%20%20%20%20return%20ProofStatus%2C%20model_hash%2C%20proof_results%2C%20proofs%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(ProofStatus%2C%20mo%2C%20proof_results%2C%20proofs)%3A%0A%20%20%20%20_rows%20%3D%20%5B%5D%0A%20%20%20%20for%20_req_id%20in%20sorted(proofs.keys())%3A%0A%20%20%20%20%20%20%20%20_script%20%3D%20proofs%5B_req_id%5D%0A%20%20%20%20%20%20%20%20_result%20%3D%20proof_results%5B_req_id%5D%0A%20%20%20%20%20%20%20%20_status%20%3D%20%22VERIFIED%22%20if%20_result.status%20%3D%3D%20ProofStatus.VERIFIED%20else%20%22FAILED%22%0A%20%20%20%20%20%20%20%20_lemmas%20%3D%20%22%2C%20%22.join(l.name%20for%20l%20in%20_script.lemmas)%0A%20%20%20%20%20%20%20%20_rows.append(f%22%7C%20%7B_req_id%7D%20%7C%20%7B_status%7D%20%7C%20%7B_script.claim%5B%3A60%5D%7D...%20%7C%20%7B_lemmas%7D%20%7C%22)%0A%0A%20%20%20%20_proof_table%20%3D%20%22%5Cn%22.join(_rows)%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%7C%20Requirement%20%7C%20Status%20%7C%20Claim%20%7C%20Lemmas%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C-------------%7C--------%7C-------%7C--------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7B_proof_table%7D%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22All%20proofs%20pass.%20Each%20can%20be%20serialized%20to%20JSON%2C%20stored%2C%20and%20re-verified%20%22%0A%20%20%20%20%20%20%20%20%22by%20anyone%20%E2%80%94%20no%20trust%20in%20the%20original%20analyst%20required.%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%203%3A%20Numerical%20Simulation%0A%0A%20%20%20%20Symbolic%20analysis%20tells%20us%20what%20the%20model%20*should*%20do.%20Numerical%0A%20%20%20%20simulation%20shows%20what%20it%20*actually%20does*%20when%20we%20integrate%20the%20full%0A%20%20%20%20nonlinear%20dynamics.%20We%20run%20two%20scenarios%3A%0A%0A%20%20%20%201.%20**Step%20response**%20%E2%80%94%2010-degree%20initial%20attitude%20error%2C%20observe%20settling%0A%20%20%20%202.%20**Disturbance%20rejection**%20%E2%80%94%20near-zero%20error%2C%20observe%20gravity%20gradient%20effects%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(params)%3A%0A%20%20%20%20from%20analysis.numerical%20import%20run_step_response%2C%20run_disturbance_rejection%0A%0A%20%20%20%20step_result%20%3D%20run_step_response(params)%0A%20%20%20%20step_summary%20%3D%20step_result.summary()%0A%0A%20%20%20%20dist_result%20%3D%20run_disturbance_rejection(params)%0A%20%20%20%20dist_summary%20%3D%20dist_result.summary()%0A%20%20%20%20return%20dist_summary%2C%20step_result%2C%20step_summary%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20step_result%2C%20step_summary)%3A%0A%20%20%20%20import%20matplotlib.pyplot%20as%20plt%0A%20%20%20%20import%20numpy%20as%20np%0A%0A%20%20%20%20_fig%2C%20_axes%20%3D%20plt.subplots(2%2C%202%2C%20figsize%3D(12%2C%208))%0A%20%20%20%20_axis_colors%20%3D%20%7B%22X%22%3A%20%22%231f77b4%22%2C%20%22Y%22%3A%20%22%232ca02c%22%2C%20%22Z%22%3A%20%22%239467bd%22%7D%20%20%23%20blue%2C%20green%2C%20purple%0A%20%20%20%20_limit_color%20%3D%20%22%23d62728%22%20%20%23%20red%20reserved%20exclusively%20for%20requirement%20limits%0A%0A%20%20%20%20%23%20Attitude%20error%0A%20%20%20%20_q_vec%20%3D%20np.linalg.norm(step_result.q%5B%3A%2C%20%3A3%5D%2C%20axis%3D1)%0A%20%20%20%20_theta_deg%20%3D%20np.degrees(2%20*%20_q_vec)%0A%20%20%20%20_axes%5B0%2C%200%5D.semilogy(step_result.t%2C%20_theta_deg%2C%20color%3D_axis_colors%5B%22X%22%5D%2C%20linewidth%3D1.5%2C%20label%3D'Attitude%20error')%0A%20%20%20%20_axes%5B0%2C%200%5D.axhline(0.1%2C%20color%3D_limit_color%2C%20linestyle%3D'--'%2C%20linewidth%3D1%2C%20label%3D'REQ-001%20limit%20(0.1%20deg)')%0A%20%20%20%20_axes%5B0%2C%200%5D.set_xlabel('Time%20(s)')%0A%20%20%20%20_axes%5B0%2C%200%5D.set_ylabel('Attitude%20Error%20(deg)')%0A%20%20%20%20_axes%5B0%2C%200%5D.set_title('Pointing%20Convergence')%0A%20%20%20%20_axes%5B0%2C%200%5D.set_ylim(bottom%3D1e-3)%0A%20%20%20%20_axes%5B0%2C%200%5D.legend(fontsize%3D8)%0A%20%20%20%20_axes%5B0%2C%200%5D.grid(True%2C%20alpha%3D0.3%2C%20which%3D'both')%0A%0A%20%20%20%20%23%20Angular%20velocity%0A%20%20%20%20for%20_i%2C%20(_axis%2C%20_c)%20in%20enumerate(_axis_colors.items())%3A%0A%20%20%20%20%20%20%20%20_axes%5B0%2C%201%5D.plot(step_result.t%2C%20np.degrees(step_result.omega%5B%3A%2C%20_i%5D)%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20color%3D_c%2C%20linewidth%3D1%2C%20label%3Df'%7B_axis%7D-axis')%0A%20%20%20%20_axes%5B0%2C%201%5D.set_xlabel('Time%20(s)')%0A%20%20%20%20_axes%5B0%2C%201%5D.set_ylabel('Angular%20Rate%20(deg%2Fs)')%0A%20%20%20%20_axes%5B0%2C%201%5D.set_title('Angular%20Velocity')%0A%20%20%20%20_axes%5B0%2C%201%5D.legend(fontsize%3D8)%0A%20%20%20%20_axes%5B0%2C%201%5D.grid(True%2C%20alpha%3D0.3)%0A%0A%20%20%20%20%23%20Control%20torque%0A%20%20%20%20for%20_i%2C%20(_axis%2C%20_c)%20in%20enumerate(_axis_colors.items())%3A%0A%20%20%20%20%20%20%20%20_axes%5B1%2C%200%5D.plot(step_result.t%2C%20step_result.tau_ctrl%5B%3A%2C%20_i%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20color%3D_c%2C%20linewidth%3D1%2C%20label%3Df'%7B_axis%7D-axis')%0A%20%20%20%20_axes%5B1%2C%200%5D.axhline(step_result.config.max_torque%2C%20color%3D_limit_color%2C%20linestyle%3D'--'%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20linewidth%3D1%2C%20alpha%3D0.7%2C%20label%3D'Torque%20limit')%0A%20%20%20%20_axes%5B1%2C%200%5D.axhline(-step_result.config.max_torque%2C%20color%3D_limit_color%2C%20linestyle%3D'--'%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20linewidth%3D1%2C%20alpha%3D0.7)%0A%20%20%20%20_axes%5B1%2C%200%5D.set_xlabel('Time%20(s)')%0A%20%20%20%20_axes%5B1%2C%200%5D.set_ylabel('Torque%20(N.m)')%0A%20%20%20%20_axes%5B1%2C%200%5D.set_title('Control%20Torque')%0A%20%20%20%20_axes%5B1%2C%200%5D.legend(fontsize%3D8)%0A%20%20%20%20_axes%5B1%2C%200%5D.grid(True%2C%20alpha%3D0.3)%0A%0A%20%20%20%20%23%20Wheel%20momentum%0A%20%20%20%20_h_mag%20%3D%20np.linalg.norm(step_result.h_wheel%2C%20axis%3D1)%0A%20%20%20%20_axes%5B1%2C%201%5D.plot(step_result.t%2C%20_h_mag%2C%20color%3D_axis_colors%5B%22X%22%5D%2C%20linewidth%3D1.5%2C%20label%3D'%7Ch%7C%20(total)')%0A%20%20%20%20_axes%5B1%2C%201%5D.axhline(step_result.config.max_momentum%2C%20color%3D_limit_color%2C%20linestyle%3D'--'%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20linewidth%3D1%2C%20label%3D'REQ-002%20limit%20(4.0%20N.m.s)')%0A%20%20%20%20_axes%5B1%2C%201%5D.set_xlabel('Time%20(s)')%0A%20%20%20%20_axes%5B1%2C%201%5D.set_ylabel('Momentum%20(N.m.s)')%0A%20%20%20%20_axes%5B1%2C%201%5D.set_title('Wheel%20Angular%20Momentum')%0A%20%20%20%20_axes%5B1%2C%201%5D.legend(fontsize%3D8)%0A%20%20%20%20_axes%5B1%2C%201%5D.grid(True%2C%20alpha%3D0.3)%0A%0A%20%20%20%20_fig.suptitle('Step%20Response%3A%2010-degree%20Slew%20Maneuver'%2C%20fontsize%3D14%2C%20fontweight%3D'bold')%0A%20%20%20%20plt.tight_layout()%0A%0A%20%20%20%20mo.md(f%22%22%22%0A%20%20%20%20%23%23%23%20Step%20Response%20Results%0A%0A%20%20%20%20%7C%20Metric%20%7C%20Value%20%7C%0A%20%20%20%20%7C--------%7C-------%7C%0A%20%20%20%20%7C%20Final%20pointing%20error%20%7C%20%7Bstep_summary%5B'final_error_deg'%5D%3A.4f%7D%20deg%20%7C%0A%20%20%20%20%7C%20Peak%20pointing%20error%20%7C%20%7Bstep_summary%5B'peak_error_deg'%5D%3A.1f%7D%20deg%20%7C%0A%20%20%20%20%7C%20Settling%20time%20%7C%20%7Bstep_summary%5B'settling_time_s'%5D%3A.1f%7D%20s%20%7C%0A%20%20%20%20%7C%20Peak%20wheel%20momentum%20%7C%20%7Bstep_summary%5B'peak_wheel_momentum'%5D%3A.3f%7D%20N.m.s%20%7C%0A%20%20%20%20%7C%20Peak%20control%20torque%20%7C%20%7Bstep_summary%5B'peak_control_torque'%5D%3A.4f%7D%20N.m%20%7C%0A%20%20%20%20%22%22%22)%0A%0A%20%20%20%20_fig%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(dist_summary%2C%20mo)%3A%0A%20%20%20%20mo.md(f%22%22%22%0A%20%20%20%20%23%23%23%20Disturbance%20Rejection%20Results%0A%0A%20%20%20%20%7C%20Metric%20%7C%20Value%20%7C%0A%20%20%20%20%7C--------%7C-------%7C%0A%20%20%20%20%7C%20Peak%20error%20(GG%20disturbance)%20%7C%20%7Bdist_summary%5B'peak_error_deg'%5D%3A.6f%7D%20deg%20%7C%0A%20%20%20%20%7C%20Final%20angular%20rate%20%7C%20%7Bdist_summary%5B'final_omega_norm'%5D%3A.2e%7D%20rad%2Fs%20%7C%0A%0A%20%20%20%20Gravity%20gradient%20effects%20are%20negligible%20at%20GEO%20%E2%80%94%20confirming%20REQ-004.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%204%3A%20Evidence%20Binding%0A%0A%20%20%20%20Now%20we%20bind%20our%20computational%20results%20to%20the%20RDF%20traceability%20graph.%0A%20%20%20%20Every%20evidence%20artifact%20gets%20a%20content%20hash%2C%20a%20model%20hash%20(binding%20it%0A%20%20%20%20to%20the%20structural%20model%20version)%2C%20and%20PROV-O%20provenance%20(who%2Fwhat%0A%20%20%20%20produced%20it%2C%20when).%0A%0A%20%20%20%20Each%20evidence%20artifact%20**addresses**%20a%20specific%20requirement%20%E2%80%94%20recording%0A%20%20%20%20the%20structural%20intent%20that%20%22this%20proof%20was%20constructed%20to%20evaluate%0A%20%20%20%20REQ-003.%22%20But%20%60rtm%3Aaddresses%60%20is%20not%20%60rtm%3Aattests%60.%20The%20evidence%0A%20%20%20%20says%20*what%20was%20analyzed*%3B%20only%20human%20attestation%20says%20*whether%20it's%0A%20%20%20%20sufficient*.%20An%20evidence%20artifact%20can%20address%20a%20requirement%20and%20still%0A%20%20%20%20lead%20to%20a%20declined%20attestation%20%E2%80%94%20as%20we'll%20see%20with%20REQ-001.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(dist_summary%2C%20mo%2C%20model_hash%2C%20params%2C%20proofs%2C%20step_summary)%3A%0A%20%20%20%20from%20evidence.binding%20import%20bind_proof_evidence%2C%20bind_simulation_evidence%2C%20bind_computation_engines%0A%20%20%20%20from%20evidence.hashing%20import%20hash_proof%20as%20_hp%2C%20hash_evidence%2C%20hash_simulation%0A%20%20%20%20from%20pipeline.dataset%20import%20graph_for%2C%20triples_by_graph%0A%20%20%20%20from%20traceability.rtm%20import%20load_base_dataset%2C%20validate_evidence_completeness%0A%0A%20%20%20%20%23%20rtm_graph%20is%20now%20an%20rdflib.Dataset%20with%20named%20graphs.%20Existing%0A%20%20%20%20%23%20SPARQL%20queries%20still%20work%20via%20default_union%3B%20new%20audit%20%2F%20closure-%0A%20%20%20%20%23%20rule%20%2F%20backend%20code%20uses%20the%20explicit%20named-graph%20views.%0A%20%20%20%20rtm_graph%20%3D%20load_base_dataset()%0A%20%20%20%20_ev%20%3D%20graph_for(rtm_graph%2C%20%22evidence%22)%0A%20%20%20%20bind_computation_engines(_ev)%0A%0A%20%20%20%20for%20_rid%2C%20_script%20in%20proofs.items()%3A%0A%20%20%20%20%20%20%20%20_ph%20%3D%20_hp(_script%2C%20model_hash)%0A%20%20%20%20%20%20%20%20_ch%20%3D%20hash_evidence(model_hash%2C%20proof_hash%3D_ph)%0A%20%20%20%20%20%20%20%20bind_proof_evidence(%0A%20%20%20%20%20%20%20%20%20%20%20%20_ev%2C%20f%22EV-PROOF-%7B_rid%7D%22%2C%20f%22SA-%7B_rid%7D%22%2C%20_rid%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20model_hash%2C%20_ph%2C%20_ch%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20f%22Symbolic%20proof%3A%20%7B_script.claim%7D%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20source_file%3D%22analysis%2Fbuild_proofs.py%22%2C%0A%20%20%20%20%20%20%20%20)%0A%0A%20%20%20%20_sh%20%3D%20hash_simulation(%7B%22type%22%3A%20%22step_response%22%7D%2C%20step_summary)%0A%20%20%20%20for%20_rid%2C%20_desc%20in%20%5B%0A%20%20%20%20%20%20%20%20(%22REQ-001%22%2C%20f%22Step%20response%3A%20settling%3D%7Bstep_summary%5B'settling_time_s'%5D%3A.1f%7Ds%2C%20final_error%3D%7Bstep_summary%5B'final_error_deg'%5D%3A.4f%7D%20deg%22)%2C%0A%20%20%20%20%20%20%20%20(%22REQ-002%22%2C%20f%22Peak%20wheel%20momentum%3A%20%7Bstep_summary%5B'peak_wheel_momentum'%5D%3A.3f%7D%20N.m.s%20(limit%3D%7Bparams%5B'maxMomentum'%5D%7D)%22)%2C%0A%20%20%20%20%5D%3A%0A%20%20%20%20%20%20%20%20bind_simulation_evidence(%0A%20%20%20%20%20%20%20%20%20%20%20%20_ev%2C%20f%22EV-SIM-%7B_rid%7D%22%2C%20f%22NS-%7B_rid%7D%22%2C%20_rid%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20model_hash%2C%20_sh%2C%20_desc%2C%20source_file%3D%22analysis%2Fnumerical.py%22%2C%0A%20%20%20%20%20%20%20%20)%0A%0A%20%20%20%20_dh%20%3D%20hash_simulation(%7B%22type%22%3A%20%22disturbance_rejection%22%7D%2C%20dist_summary)%0A%20%20%20%20bind_simulation_evidence(%0A%20%20%20%20%20%20%20%20_ev%2C%20%22EV-SIM-REQ-004%22%2C%20%22NS-REQ-004%22%2C%20%22REQ-004%22%2C%0A%20%20%20%20%20%20%20%20model_hash%2C%20_dh%2C%0A%20%20%20%20%20%20%20%20f%22Disturbance%20rejection%3A%20peak_error%3D%7Bdist_summary%5B'peak_error_deg'%5D%3A.6f%7D%20deg%22%2C%0A%20%20%20%20%20%20%20%20source_file%3D%22analysis%2Fnumerical.py%22%2C%0A%20%20%20%20)%0A%0A%20%20%20%20_issues%20%3D%20validate_evidence_completeness(rtm_graph)%0A%20%20%20%20_counts%20%3D%20triples_by_graph(rtm_graph)%0A%0A%20%20%20%20_count_rows%20%3D%20%22%5Cn%22.join(%0A%20%20%20%20%20%20%20%20f%22%7C%20%60%3C%7B_iri.rsplit('%2F'%2C%201)%5B-1%5D%7D%3E%60%20%7C%20%7B_n%7D%20%7C%22%0A%20%20%20%20%20%20%20%20for%20_iri%2C%20_n%20in%20sorted(_counts.items())%0A%20%20%20%20)%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Evidence%20artifacts%20in%20their%20named%20graph%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22-%20**4%20proof%20artifacts**%20(hash-bound%20to%20model%20%60%7Bmodel_hash%5B%3A16%5D%7D...%60)%5Cn%22%0A%20%20%20%20%20%20%20%20f%22-%20**3%20simulation%20results**%5Cn%22%0A%20%20%20%20%20%20%20%20f%22-%20All%20emitted%20into%20%60%3Cadcs%3Aevidence%3E%60%20%E2%80%94%20kept%20distinct%20from%20the%20structural%20%22%0A%20%20%20%20%20%20%20%20f%22and%20ontology%20layers%20so%20SPARQL%20queries%20can%20scope%20by%20graph%2C%20and%20the%20%22%0A%20%20%20%20%20%20%20%20f%22Phase%20J%20Flexo%20backend%20can%20push%20each%20layer%20as%20its%20own%20branch.%5Cn%22%0A%20%20%20%20%20%20%20%20f%22-%20Evidence%20completeness%3A%20**%7B'PASS'%20if%20not%20_issues%20else%20'ISSUES%3A%20'%20%2B%20str(_issues)%7D**%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**Per-graph%20triple%20counts%20after%20Act%204%3A**%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Named%20graph%20%7C%20Triples%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C---%7C---%3A%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%2B%20_count_rows%20%2B%20%22%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22Every%20artifact%20carries%20%60rtm%3AcontentHash%60%2C%20%60rtm%3AmodelHash%60%2C%20and%20a%20%22%0A%20%20%20%20%20%20%20%20%22PROV-O%20provenance%20chain.%20The%20model%20hash%20ensures%20that%20if%20the%20model%20%22%0A%20%20%20%20%20%20%20%20%22changes%20(Act%208)%2C%20all%20evidence%20must%20be%20re-produced%20and%20re-verified.%22%0A%20%20%20%20)%0A%20%20%20%20return%20(rtm_graph%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%205%3A%20Attestation%20(GSN%20%2B%20EARL%20outcomes)%0A%0A%20%20%20%20Evidence%20alone%20doesn't%20satisfy%20requirements.%20The%20engineer%20makes%20two%0A%20%20%20%20judgments%20per%20requirement%20%E2%80%94%20and%20we%20record%20them%20using%20**established%0A%20%20%20%20assurance-case%20vocabulary**%2C%20not%20novel%20terms%3A%0A%0A%20%20%20%20-%20**Adequacy**%20%E2%86%92%20a%20%60gsn%3AAssumption%60%20(Hawkins%E2%80%93Habli%20%22asserted%20context%22)%0A%20%20%20%20%20%20stating%20the%20model%20adequately%20represents%20the%20physical%20system%20for%0A%20%20%20%20%20%20this%20requirement.%20Text%20on%20%60gsn%3Astatement%60.%0A%20%20%20%20-%20**Sufficiency**%20%E2%86%92%20a%20%60gsn%3AJustification%60%20(Hawkins%E2%80%93Habli%20%22asserted%0A%20%20%20%20%20%20inference%22)%20stating%20the%20evidence%20is%20sufficient%20to%20conclude%0A%20%20%20%20%20%20satisfaction.%20Text%20on%20%60gsn%3Astatement%60.%0A%20%20%20%20-%20**Outcome**%20%E2%86%92%20an%20%60earl%3Aoutcome%60%20from%20EARL's%20five-valued%20lattice%3A%0A%20%20%20%20%20%20%60earl%3Apassed%60%20%2F%20%60earl%3Afailed%60%20%2F%20%60earl%3AcantTell%60%20%2F%20%60earl%3Ainapplicable%60%0A%20%20%20%20%20%20%2F%20%60earl%3Auntested%60.%20Better%20than%20binary%20pass%2Ffail%20because%20%22models%20are%0A%20%20%20%20%20%20imperfect%22%20%E2%80%94%20%60cantTell%60%20and%20%60inapplicable%60%20are%20first-class.%0A%20%20%20%20-%20**Qualified%20association**%20%E2%86%92%20a%20%60prov%3AAssociation%60%20carrying%20the%0A%20%20%20%20%20%20engineer's%20%60prov%3AhadRole%60%20(%60rtm%3Arole-AttestingEngineer%60)%20and%20the%0A%20%20%20%20%20%20%60prov%3AhadPlan%60%20they%20followed%20(the%20standard%20attestation%20procedure).%0A%0A%20%20%20%20REQ-001%20below%20is%20**attested-with-failed**%2C%20not%20silently%20omitted%20%E2%80%94%0A%20%20%20%20the%20audit%20trail%20records%20the%20declination%20as%20a%20well-formed%20attestation%0A%20%20%20%20so%20closure-rule%20shapes%20can%20validate%20against%20an%20audit-complete%20graph.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20params%2C%20rtm_graph%2C%20step_summary)%3A%0A%20%20%20%20from%20traceability.attestation%20import%20request_attestation%2C%20OUTCOME_FAILED%0A%0A%20%20%20%20_adequacy%20%3D%20%7B%0A%20%20%20%20%20%20%20%20%22REQ-001%22%3A%20(%22Step-response%20simulation%20is%20adequate%20for%20evaluating%20pointing-%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22accuracy%20settling%20time%20at%20this%20point%20in%20the%20lifecycle.%22)%2C%0A%20%20%20%20%20%20%20%20%22REQ-002%22%3A%20(%22Energy-based%20momentum%20bound%20is%20conservative.%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22Reaction%20wheel%20model%20adequate%20for%20peak%20momentum%20estimation.%22)%2C%0A%20%20%20%20%20%20%20%20%22REQ-003%22%3A%20(%22Linearized%20stability%20analysis%20via%20Routh-Hurwitz%20is%20adequate%20for%20this%20design%20point.%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22Nonlinear%20effects%20are%20second-order%20for%20small%20angles%20around%20the%20operating%20point.%22)%2C%0A%20%20%20%20%20%20%20%20%22REQ-004%22%3A%20(%22Linearized%20gravity%20gradient%20model%20adequate%20for%20GEO%20orbit.%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22Higher-order%20terms%20negligible%20at%20geostationary%20altitude.%22)%2C%0A%20%20%20%20%7D%0A%20%20%20%20_sufficiency%20%3D%20%7B%0A%20%20%20%20%20%20%20%20%22REQ-001%22%3A%20(f%22Evidence%20is%20sufficient%20to%20conclude%20REQ-001%20is%20NOT%20yet%20satisfied%3A%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20f%22settling%20time%20%7Bstep_summary%5B'settling_time_s'%5D%3A.0f%7Ds%20exceeds%20the%20120s%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20f%22requirement.%20Action%20item%3A%20retune%20gains%20(Kp%3A%20%7Bparams%5B'Kp'%5D%3A.0f%7D%E2%86%924%2C%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20f%22Kd%3A%20%7Bparams%5B'Kd'%5D%3A.0f%7D%E2%86%9230)%20and%20re-verify.%22)%2C%0A%20%20%20%20%20%20%20%20%22REQ-002%22%3A%20(%22Both%20symbolic%20bound%20(0.81%20N.m.s)%20and%20numerical%20simulation%20confirm%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22peak%20momentum%20well%20below%204.0%20N.m.s%20rated%20capacity.%20Large%20margin.%22)%2C%0A%20%20%20%20%20%20%20%20%22REQ-003%22%3A%20(%22Routh-Hurwitz%20proof%20confirms%20asymptotic%20stability%20for%20ALL%20positive%20J%2C%20Kp%2C%20Kd%20%E2%80%94%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22this%20is%20a%20parametric%20result%2C%20not%20just%20for%20one%20design%20point.%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22Numerical%20eigenvalues%20confirm%20margins%20exceed%20-0.010%20rad%2Fs%20on%20all%20axes.%22)%2C%0A%20%20%20%20%20%20%20%20%22REQ-004%22%3A%20(%22Gravity%20gradient%20torques%20at%20GEO%20are%20~1e-6%20N.m%2C%20four%20orders%20of%20magnitude%20below%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%220.1%20N.m%20actuator%20capacity.%20Simulation%20confirms%20negligible%20pointing%20impact.%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22Overwhelming%20margin.%22)%2C%0A%20%20%20%20%7D%0A%0A%20%20%20%20%23%20REQ-001%3A%20explicit%20DECLINATION%20as%20earl%3Afailed%20%E2%80%94%20keeps%20the%20audit%0A%20%20%20%20%23%20trail%20complete%20so%20the%20closure-rule%20suite%20validates.%0A%20%20%20%20request_attestation(%0A%20%20%20%20%20%20%20%20rtm_graph%2C%20%22REQ-001%22%2C%20%22Dr.%20Michael%20Zargham%20(%40mzargham)%22%2C%0A%20%20%20%20%20%20%20%20auto_attest%3DTrue%2C%0A%20%20%20%20%20%20%20%20model_adequacy%3D_adequacy%5B%22REQ-001%22%5D%2C%0A%20%20%20%20%20%20%20%20evidence_sufficiency%3D_sufficiency%5B%22REQ-001%22%5D%2C%0A%20%20%20%20%20%20%20%20outcome%3DOUTCOME_FAILED%2C%0A%20%20%20%20)%0A%0A%20%20%20%20%23%20REQ-002%2C%20REQ-003%2C%20REQ-004%20%E2%80%94%20outcome%20defaults%20to%20earl%3Apassed%0A%20%20%20%20for%20_rid%20in%20%5B%22REQ-002%22%2C%20%22REQ-003%22%2C%20%22REQ-004%22%5D%3A%0A%20%20%20%20%20%20%20%20request_attestation(%0A%20%20%20%20%20%20%20%20%20%20%20%20rtm_graph%2C%20_rid%2C%20%22Dr.%20Michael%20Zargham%20(%40mzargham)%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20auto_attest%3DTrue%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20model_adequacy%3D_adequacy%5B_rid%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20evidence_sufficiency%3D_sufficiency%5B_rid%5D%2C%0A%20%20%20%20%20%20%20%20)%0A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20%23%23%23%20Attestation%20outcomes%0A%0A%20%20%20%20%7C%20Requirement%20%7C%20Outcome%20%7C%20Reasoning%20%7C%0A%20%20%20%20%7C---%7C---%7C---%7C%0A%20%20%20%20%7C%20REQ-001%20%7C%20%60earl%3Afailed%60%20%20%20%7C%20Settling%20time%20~262s%20%3E%20120s%20requirement%3B%20action%20item%20recorded%20%7C%0A%20%20%20%20%7C%20REQ-002%20%7C%20%60earl%3Apassed%60%20%20%20%7C%20Peak%20momentum%20well%20within%204.0%20N.m.s%20%7C%0A%20%20%20%20%7C%20REQ-003%20%7C%20%60earl%3Apassed%60%20%20%20%7C%20Routh-Hurwitz%20parametric%20stability%20proof%20%7C%0A%20%20%20%20%7C%20REQ-004%20%7C%20%60earl%3Apassed%60%20%20%20%7C%20Gravity%20gradient%20torques%204%20orders%20below%20actuator%20capacity%20%7C%0A%0A%20%20%20%20All%20four%20attestations%20are%20well-formed%3A%20each%20carries%20an%20adequacy%0A%20%20%20%20%60gsn%3AAssumption%60%2C%20a%20sufficiency%20%60gsn%3AJustification%60%2C%20an%20EARL%20outcome%2C%0A%20%20%20%20a%20qualified%20association%20naming%20the%20engineer's%20role%20and%20the%20procedure%0A%20%20%20%20followed%2C%20and%20references%20to%20the%20evidence%20consulted.%20REQ-001%20is%0A%20%20%20%20*attested%20with%20%60earl%3Afailed%60*%20%E2%80%94%20the%20audit%20graph%20records%20the%20gap%0A%20%20%20%20explicitly%20rather%20than%20hiding%20it%20as%20%22missing.%22%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%206%3A%20Closure-Rule%20Validation%20%2B%20Audit%20(initial)%0A%0A%20%20%20%20Before%20the%20program's%20chief%20systems%20engineer%20reviews%20the%20work%2C%20two%0A%20%20%20%20automated%20checks%20ratify%20that%20the%20RTM%20graph%20itself%20is%20well-formed%20and%0A%20%20%20%20internally%20consistent%3A%0A%0A%20%20%20%201.%20**Closure-rule%20suite%20(SHACL).**%20Ten%20machine-checkable%20invariants%20%E2%80%94%0A%20%20%20%20%20%20%20every%20attestation%20has%20both%20an%20adequacy%20Assumption%20and%20a%20sufficiency%0A%20%20%20%20%20%20%20Justification%2C%20every%20evidence%20artifact%20has%20hashes%20and%20references%20a%0A%20%20%20%20%20%20%20requirement%2C%20every%20analysis%20activity%20has%20an%20associated%20agent%2C%20etc.%0A%20%20%20%20%20%20%20Plus%20a%20runtime%20re-verification%20check%20that%20re-hashes%20every%20proof.%0A%20%20%20%202.%20**Forward%20%2F%20Backward%20%2F%20Bidirectional%20audit.**%20Forward%20and%20backward%0A%20%20%20%20%20%20%20run%20*independently*%20so%20the%20failure%20mode%20names%20which%20direction%0A%20%20%20%20%20%20%20broke.%20Bidirectional%20is%20the%20derived%20conjunction.%0A%0A%20%20%20%20If%20any%20closure%20rule%20fails%2C%20the%20audit%20module's%20%22fresh%20graph%22%20claim%0A%20%20%20%20can't%20be%20trusted.%20The%20two%20checks%20together%20are%20what%20an%20auditor%20would%0A%20%20%20%20run%20before%20asking%20any%20substantive%20question.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20rtm_graph)%3A%0A%20%20%20%20from%20traceability.validation%20import%20validate%20as%20_validate%0A%0A%20%20%20%20_report%20%3D%20_validate(rtm_graph%2C%20skip_reverification%3DFalse)%0A%0A%20%20%20%20_summary%20%3D%20%22%5Cn%22.join(%22%20%20%20%20%22%20%2B%20l%20for%20l%20in%20_report.summary_lines())%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Closure-rule%20suite%20(Stage%206.5)%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7B_summary%7D%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22Ten%20invariants%20enforced%20%E2%80%94%20nine%20SHACL%20shapes%20%2B%20one%20runtime%20%22%0A%20%20%20%20%20%20%20%20%22re-verification%20check.%20The%20shapes%20target%20distinct%20layers%20of%20the%20%22%0A%20%20%20%20%20%20%20%20%22graph%3A%20attestation%20well-formedness%2C%20plan-instantiation%20correctness%2C%20%22%0A%20%20%20%20%20%20%20%20%22evidence%20completeness%2C%20requirement%20structure%2C%20GSN%20argument%20well-%22%0A%20%20%20%20%20%20%20%20%22formedness%2C%20PROV%20provenance%20shape%2C%20outcome%20semantics%2C%20%22%0A%20%20%20%20%20%20%20%20%22forward%2Fbackward%20traceability%2C%20and%20named-graph%20integrity.%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20rtm_graph)%3A%0A%20%20%20%20from%20traceability.audit%20import%20audit%20as%20_audit_fn%2C%20render_report%20as%20_render%0A%0A%20%20%20%20audit_report%20%3D%20_audit_fn(rtm_graph)%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Audit%20(Stage%207a)%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%20%20%20%20%7Baudit_report.forward.summary()%7D%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%20%20%20%20%7Baudit_report.backward.summary()%7D%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%20%20%20%20Bidirectional%3A%20%7B'PASS'%20if%20audit_report.bidirectional().passed%20else%20'FAIL'%7D%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%20%20%20%20Orphans%3A%20%7B'none'%20if%20not%20audit_report.orphans.any%20else%20'see%20report'%7D%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**Two%20orthogonal%20questions%2C%20not%20one.**%20The%20audit%20decouples%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22-%20**traceability**%20%E2%80%94%20*is%20the%20structural%20chain%20intact%3F*%20%22%0A%20%20%20%20%20%20%20%20%22Forward%20asks%20if%20every%20requirement%20is%20reached%20by%20evidence%20%2B%20an%20%22%0A%20%20%20%20%20%20%20%20%22attestation%3B%20backward%20asks%20if%20every%20attestation's%20evidence%20%22%0A%20%20%20%20%20%20%20%20%22actually%20addresses%20its%20claimed%20requirement.%20Bidirectional%20is%20%22%0A%20%20%20%20%20%20%20%20%22the%20conjunction.%20These%20are%20structural%20facts%20about%20the%20graph.%5Cn%22%0A%20%20%20%20%20%20%20%20%22-%20**coverage%20status**%20%E2%80%94%20*is%20the%20requirement%20satisfied%3F*%20%22%0A%20%20%20%20%20%20%20%20%22Outcome-derived%20per%20cell%20of%20the%20coverage%20matrix%3A%20%22%0A%20%20%20%20%20%20%20%20%22%60covered%2Bpassed%60%20%2F%20%60covered%2Bfailed%60%20%2F%20%60covered%2BcantTell%60%20%2F%20%22%0A%20%20%20%20%20%20%20%20%22%60uncovered%60.%20These%20are%20the%20engineering%20verdicts%20captured%20in%20%22%0A%20%20%20%20%20%20%20%20%22each%20attestation's%20%60earl%3Aoutcome%60.%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**The%20v1%20verdict%20(this%20stage).**%20Traceability%20passes%20%E2%80%94%20the%20%22%0A%20%20%20%20%20%20%20%20%22chain%20is%20structurally%20sound%2C%20no%20orphans%2C%20every%20attestation%20%22%0A%20%20%20%20%20%20%20%20%22lines%20up%20with%20its%20evidence.%20**REQ-001%20is%20%60covered%2Bfailed%60%20and%20%22%0A%20%20%20%20%20%20%20%20%22this%20is%20the%20*expected*%20output%20of%20v1**%3A%20the%20engineering%20analysis%20%22%0A%20%20%20%20%20%20%20%20%22produced%20a%20real%20finding%20(settling%20time%20%3E%20spec)%20and%20the%20audit%20%22%0A%20%20%20%20%20%20%20%20%22surfaces%20it%20as%20a%20coverage%20gap%20rather%20than%20hiding%20it%20behind%20%22%0A%20%20%20%20%20%20%20%20%22'unattested'.%20Act%208%20%E2%80%94%20Design%20Iteration%20%E2%80%94%20is%20the%20response%2C%20and%20%22%0A%20%20%20%20%20%20%20%20%22Act%2010's%20audit%20shows%20the%20same%20matrix%20flipping%20to%20all%20%22%0A%20%20%20%20%20%20%20%20%22%60covered%2Bpassed%60.%22%0A%20%20%20%20)%0A%20%20%20%20return%20(audit_report%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(audit_report%2C%20mo)%3A%0A%20%20%20%20_rows%20%3D%20%22%5Cn%22.join(%0A%20%20%20%20%20%20%20%20f%22%7C%20%7Bc.requirement%7D%20%7C%20%7Bc.evidence%7D%20%7C%20%7Bc.status%7D%20%7C%22%0A%20%20%20%20%20%20%20%20for%20c%20in%20audit_report.coverage%0A%20%20%20%20)%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22**Coverage%20matrix**%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Requirement%20%7C%20Evidence%20%7C%20Status%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C---%7C---%7C---%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%2B%20_rows%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(rtm_graph)%3A%0A%20%20%20%20from%20interrogate.explain%20import%20explain_requirement%0A%0A%20%20%20%20explanations%20%3D%20%7B%7D%0A%20%20%20%20for%20_rid%20in%20%5B%22REQ-001%22%2C%20%22REQ-002%22%2C%20%22REQ-003%22%2C%20%22REQ-004%22%5D%3A%0A%20%20%20%20%20%20%20%20explanations%5B_rid%5D%20%3D%20explain_requirement(rtm_graph%2C%20_rid)%0A%20%20%20%20return%20(explanations%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(explanations%2C%20mo)%3A%0A%20%20%20%20mo.md(f%22%22%22%0A%20%20%20%20%23%23%23%20%22How%20do%20you%20know%20REQ-003%20is%20satisfied%3F%22%0A%0A%20%20%20%20%60%60%60%0A%20%20%20%20%7Bexplanations%5B%22REQ-003%22%5D%7D%0A%20%20%20%20%60%60%60%0A%0A%20%20%20%20The%20proof%20was%20**re-executed%20live**%20during%20this%20interrogation.%20The%20auditor%0A%20%20%20%20doesn't%20need%20to%20trust%20the%20original%20analyst%20%E2%80%94%20they%20can%20see%20each%20lemma%0A%20%20%20%20verified%20independently%2C%20right%20now.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(explanations%2C%20mo)%3A%0A%20%20%20%20mo.md(f%22%22%22%0A%20%20%20%20%23%23%23%20%22What%20does%20the%20audit%20say%20about%20REQ-001%3F%22%0A%0A%20%20%20%20%60%60%60%0A%20%20%20%20%7Bexplanations%5B%22REQ-001%22%5D%7D%0A%20%20%20%20%60%60%60%0A%0A%20%20%20%20REQ-001%20is%20**%60covered%2Bfailed%60%20at%20v1**%20%E2%80%94%20the%20structural%20trace%20from%0A%20%20%20%20requirement%20%E2%86%92%20evidence%20%E2%86%92%20attestation%20is%20complete%20(which%20is%20why%0A%20%20%20%20forward%2Fbackward%20both%20PASS)%2C%20and%20the%20engineer%20recorded%20an%0A%20%20%20%20%60earl%3Afailed%60%20outcome%20with%20a%20precise%20reason%20(settling%20time%20%3E%20spec)%0A%20%20%20%20and%20an%20action%20item%20(retune%20gains).%0A%0A%20%20%20%20This%20is%20the%20lifecycle%20state%20the%20demo%20is%20*designed*%20to%20produce%20at%0A%20%20%20%20v1.%20The%20auditor%20sees%20three%20things%20separately%3A%0A%0A%20%20%20%201.%20**The%20trace%20is%20intact.**%20No%20%22missing%20attestation%22%2C%20no%20orphan%0A%20%20%20%20%20%20%20evidence%20%E2%80%94%20the%20graph%20is%20internally%20consistent.%0A%20%20%20%202.%20**The%20engineering%20verdict%20is%20recorded.**%20Outcome%20%3D%20%60earl%3Afailed%60%2C%0A%20%20%20%20%20%20%20with%20adequacy%20and%20sufficiency%20text%20on%20linked%20GSN%20nodes.%0A%20%20%20%203.%20**The%20next%20action%20is%20in%20the%20record.**%20The%20sufficiency%0A%20%20%20%20%20%20%20%60gsn%3AJustification%60%20carries%20the%20corrective%20recommendation%2C%20so%0A%20%20%20%20%20%20%20the%20design%20iteration%20in%20Act%208%20has%20a%20documented%20starting%20point.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20rtm_graph)%3A%0A%20%20%20%20from%20interrogate.reproduce%20import%20reproduce_all_evidence%0A%0A%20%20%20%20_repro%20%3D%20reproduce_all_evidence(rtm_graph)%0A%0A%20%20%20%20_proof_rows%20%3D%20%5B%5D%0A%20%20%20%20for%20_p%20in%20_repro%5B%22proofs%22%5D%3A%0A%20%20%20%20%20%20%20%20_match%20%3D%20%22MATCH%22%20if%20_p%5B%22hash_match%22%5D%20else%20%22MISMATCH%22%0A%20%20%20%20%20%20%20%20_proof_rows.append(f%22%7C%20%7B_p%5B'requirement'%5D%7D%20%7C%20%7B_p%5B'status'%5D.value%7D%20%7C%20%7B_match%7D%20%7C%22)%0A%0A%20%20%20%20_repro_table%20%3D%20%22%5Cn%22.join(_proof_rows)%0A%20%20%20%20_n_sims%20%3D%20len(_repro%5B'simulations'%5D)%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Reproducibility%20Audit%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22The%20auditor%20re-executes%20ALL%20computational%20evidence%3A%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**Proof%20Re-verification%3A**%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Requirement%20%7C%20Status%20%7C%20Hash%20Match%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C-------------%7C--------%7C-----------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7B_repro_table%7D%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22**Simulation%20Reproduction%3A**%20%7B_n_sims%7D%20simulations%20re-run%20successfully.%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22Every%20proof%20re-verifies.%20Every%20hash%20matches.%20The%20evidence%20is%20%22%0A%20%20%20%20%20%20%20%20%22reproducible%20%E2%80%94%20not%20because%20we%20say%20so%2C%20but%20because%20the%20auditor%20%22%0A%20%20%20%20%20%20%20%20%22just%20confirmed%20it.%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%207%3A%20The%20Traceability%20Graph%0A%0A%20%20%20%20The%20complete%20v1%20RTM%20as%20a%20directed%20graph.%20Requirements%20(blue)%20flow%0A%20%20%20%20through%20design%20elements%20(green)%20to%20evidence%20(orange%2Fyellow)%20to%0A%20%20%20%20attestations%20(red).%20Every%20edge%20is%20a%20queryable%20RDF%20triple%20in%20git.%0A%0A%20%20%20%20What%20you%20should%20see%20at%20v1%3A%0A%0A%20%20%20%20-%20**All%20four%20requirements%20have%20full%20chains**%20to%20evidence%20and%20an%0A%20%20%20%20%20%20attestation%20node%20%E2%80%94%20that's%20why%20Act%206's%20audit%20reported%20the%20trace%0A%20%20%20%20%20%20as%20PASS.%20The%20chain%20is%20structurally%20complete%20for%20every%0A%20%20%20%20%20%20requirement.%0A%20%20%20%20-%20**REQ-001's%20attestation%20carries%20%60earl%3Afailed%60**%20in%20the%20outcome%20%E2%80%94%0A%20%20%20%20%20%20the%20engineering%20verdict%20%E2%80%94%20even%20though%20its%20trace%20looks%20just%20like%0A%20%20%20%20%20%20the%20other%20three%20at%20the%20graph%20level.%20Outcome%20lives%20on%20the%0A%20%20%20%20%20%20attestation%20node%20as%20a%20property%2C%20not%20in%20the%20link%20shape.%0A%0A%20%20%20%20The%20%60print_rtm_summary%60%20block%20below%20makes%20this%20distinction%0A%20%20%20%20explicit%3A%20requirements%20are%20categorized%20as%20ATTESTED%20with%20their%0A%20%20%20%20EARL%20outcome%20surfaced%2C%20separating%20%22trace%20intact%20%2B%20verdict%20pending%0A%20%20%20%20work%22%20from%20%22trace%20incomplete.%22%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(rtm_graph)%3A%0A%20%20%20%20from%20interrogate.visualize%20import%20build_rtm_figure%0A%0A%20%20%20%20rtm_fig%20%3D%20build_rtm_figure(rtm_graph%2C%20figsize%3D(18%2C%2010))%0A%20%20%20%20rtm_fig%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20rtm_graph)%3A%0A%20%20%20%20from%20traceability.rtm%20import%20print_rtm_summary%0A%0A%20%20%20%20_summary%20%3D%20print_rtm_summary(rtm_graph)%0A%20%20%20%20mo.md(f%22%22%22%0A%20%20%20%20%23%23%23%20Final%20Status%0A%0A%20%20%20%20%60%60%60%0A%20%20%20%20%7B_summary%7D%0A%20%20%20%20%60%60%60%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%208%3A%20Design%20Iteration%0A%0A%20%20%20%20The%20open%20finding%20on%20REQ-001%20drives%20action.%20We%20need%20to%20increase%20the%0A%20%20%20%20derivative%20gain%20Kd%20to%20reduce%20settling%20time.%20Rather%20than%20editing%20a%20file%0A%20%20%20%20by%20hand%2C%20we%20apply%20a%20**SPARQL%20UPDATE**%20to%20the%20structural%20model%20%E2%80%94%20the%0A%20%20%20%20same%20way%20any%20RDF-native%20toolchain%20would%20propagate%20a%20design%20change.%0A%0A%20%20%20%20This%20demonstrates%20**reproducibility%20as%20regression%20testing**%3A%20the%20model%0A%20%20%20%20hash%20changes%2C%20all%20previous%20proofs%20are%20invalidated%2C%20and%20we%20must%20re-run%0A%20%20%20%20the%20entire%20analysis%20chain%20from%20scratch.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20struct_graph)%3A%0A%20%20%20%20from%20rdflib%20import%20Literal%2C%20XSD%0A%0A%20%20%20%20%23%20Clone%20the%20graph%20for%20the%20design%20iteration%0A%20%20%20%20from%20rdflib%20import%20Graph%20as%20_G%0A%20%20%20%20from%20ontology.prefixes%20import%20bind_prefixes%20as%20_bp%2C%20SYSML%20as%20_SYSML%0A%0A%20%20%20%20v2_graph%20%3D%20_G()%0A%20%20%20%20_bp(v2_graph)%0A%20%20%20%20for%20triple%20in%20struct_graph%3A%0A%20%20%20%20%20%20%20%20v2_graph.add(triple)%0A%0A%20%20%20%20%23%20Apply%20SPARQL%20UPDATE%3A%20retune%20both%20controller%20gains%0A%20%20%20%20%23%20Increasing%20Kd%20alone%20would%20overdamp%20the%20system%20%E2%80%94%20a%20controls%20engineer%0A%20%20%20%20%23%20retunes%20both%20Kp%20(stiffness)%20and%20Kd%20(damping)%20together.%0A%20%20%20%20_sparql_update_kd%20%3D%20%22%22%22%0A%20%20%20%20DELETE%20%7B%20%3Fattr%20sysml%3Avalue%20%3FoldVal%20%7D%0A%20%20%20%20INSERT%20%7B%20%3Fattr%20sysml%3Avalue%20%2230.0%22%5E%5Exsd%3Adouble%20%7D%0A%20%20%20%20WHERE%20%7B%0A%20%20%20%20%20%20%20%20%3Fattr%20sysml%3AdeclaredName%20%22Kd%22%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20sysml%3Avalue%20%3FoldVal%20.%0A%20%20%20%20%7D%0A%20%20%20%20%22%22%22%0A%20%20%20%20_sparql_update_kp%20%3D%20%22%22%22%0A%20%20%20%20DELETE%20%7B%20%3Fattr%20sysml%3Avalue%20%3FoldVal%20%7D%0A%20%20%20%20INSERT%20%7B%20%3Fattr%20sysml%3Avalue%20%224.0%22%5E%5Exsd%3Adouble%20%7D%0A%20%20%20%20WHERE%20%7B%0A%20%20%20%20%20%20%20%20%3Fattr%20sysml%3AdeclaredName%20%22Kp%22%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20sysml%3Avalue%20%3FoldVal%20.%0A%20%20%20%20%7D%0A%20%20%20%20%22%22%22%0A%20%20%20%20v2_graph.update(_sparql_update_kd%2C%20initNs%3D%7B%22sysml%22%3A%20_SYSML%7D)%0A%20%20%20%20v2_graph.update(_sparql_update_kp%2C%20initNs%3D%7B%22sysml%22%3A%20_SYSML%7D)%0A%0A%20%20%20%20%23%20Verify%0A%20%20%20%20_check%20%3D%20%22%22%22%0A%20%20%20%20SELECT%20%3Fname%20%3Fval%20WHERE%20%7B%0A%20%20%20%20%20%20%20%20%3Fattr%20sysml%3AdeclaredName%20%3Fname%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20sysml%3Avalue%20%3Fval%20.%0A%20%20%20%20%20%20%20%20FILTER(%3Fname%20IN%20(%22Kp%22%2C%20%22Kd%22))%0A%20%20%20%20%7D%0A%20%20%20%20ORDER%20BY%20%3Fname%0A%20%20%20%20%22%22%22%0A%20%20%20%20_gains%20%3D%20%7Bstr(r%5B0%5D)%3A%20float(r%5B1%5D)%20for%20r%20in%20v2_graph.query(_check%2C%20initNs%3D%7B%22sysml%22%3A%20_SYSML%7D)%7D%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20SPARQL%20UPDATE%3A%20Controller%20Retune%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22A%20controls%20engineer%20retunes%20both%20gains%20together%20%E2%80%94%20increasing%20Kd%20alone%5Cn%22%0A%20%20%20%20%20%20%20%20%22would%20overdamp%20the%20system%2C%20making%20settling%20*slower*%20despite%20more%20damping.%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60sparql%5Cn%22%0A%20%20%20%20%20%20%20%20%22%23%20Increase%20proportional%20gain%20(stiffness)%5Cn%22%0A%20%20%20%20%20%20%20%20'DELETE%20%7B%20%3Fattr%20sysml%3Avalue%20%3FoldVal%20%7D%5Cn'%0A%20%20%20%20%20%20%20%20'INSERT%20%7B%20%3Fattr%20sysml%3Avalue%20%224.0%22%5E%5Exsd%3Adouble%20%7D%5Cn'%0A%20%20%20%20%20%20%20%20'WHERE%20%20%7B%20%3Fattr%20sysml%3AdeclaredName%20%22Kp%22%20%3B%20sysml%3Avalue%20%3FoldVal%20.%20%7D%5Cn%5Cn'%0A%20%20%20%20%20%20%20%20%22%23%20Increase%20derivative%20gain%20(damping)%5Cn%22%0A%20%20%20%20%20%20%20%20'DELETE%20%7B%20%3Fattr%20sysml%3Avalue%20%3FoldVal%20%7D%5Cn'%0A%20%20%20%20%20%20%20%20'INSERT%20%7B%20%3Fattr%20sysml%3Avalue%20%2230.0%22%5E%5Exsd%3Adouble%20%7D%5Cn'%0A%20%20%20%20%20%20%20%20'WHERE%20%20%7B%20%3Fattr%20sysml%3AdeclaredName%20%22Kd%22%20%3B%20sysml%3Avalue%20%3FoldVal%20.%20%7D%5Cn'%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Gain%20%7C%20Before%20%7C%20After%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C------%7C--------%7C-------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Kp%20%7C%201.0%20N.m%2Frad%20%7C%20**%7B_gains%5B'Kp'%5D%3A.1f%7D**%20N.m%2Frad%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Kd%20%7C%2010.0%20N.m.s%2Frad%20%7C%20**%7B_gains%5B'Kd'%5D%3A.1f%7D**%20N.m.s%2Frad%20%7C%22%0A%20%20%20%20)%0A%20%20%20%20return%20(v2_graph%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20model_hash%2C%20v2_graph)%3A%0A%20%20%20%20from%20evidence.hashing%20import%20hash_structural_model%20as%20_hsm%0A%0A%20%20%20%20v2_model_hash%20%3D%20_hsm(v2_graph)%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Model%20Hash%20Invalidation%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20%7C%20Hash%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C--%7C------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Original%20model%20%7C%20%60%7Bmodel_hash%5B%3A24%5D%7D...%60%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Updated%20model%20%20%7C%20%60%7Bv2_model_hash%5B%3A24%5D%7D...%60%20%7C%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22The%20hashes%20differ%20%E2%80%94%20**all%20previous%20proofs%20and%20evidence%20are%20now%20invalid**.%5Cn%22%0A%20%20%20%20%20%20%20%20%22Any%20attempt%20to%20verify%20an%20old%20proof%20against%20the%20new%20model%20hash%20will%20fail.%5Cn%22%0A%20%20%20%20%20%20%20%20%22We%20must%20re-derive%20everything%20from%20scratch.%22%0A%20%20%20%20)%0A%20%20%20%20return%20(v2_model_hash%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20v2_graph%2C%20v2_model_hash)%3A%0A%20%20%20%20from%20analysis.load_params%20import%20load_params%20as%20_lp%0A%20%20%20%20from%20analysis.symbolic%20import%20run_symbolic_analysis%20as%20_rsa%0A%20%20%20%20from%20analysis.build_proofs%20import%20build_all_proofs%20as%20_bap%0A%20%20%20%20from%20analysis.proof_scripts%20import%20verify_proof%20as%20_vp%2C%20ProofStatus%20as%20_PS%0A%0A%20%20%20%20v2_params%20%3D%20_lp(v2_graph)%0A%20%20%20%20v2_sym%20%3D%20_rsa(v2_params)%0A%20%20%20%20v2_margins%20%3D%20v2_sym.stability_margins%0A%0A%20%20%20%20v2_proofs%20%3D%20_bap(v2_model_hash)%0A%20%20%20%20v2_proof_results%20%3D%20%7B%7D%0A%20%20%20%20for%20_rid%2C%20_script%20in%20v2_proofs.items()%3A%0A%20%20%20%20%20%20%20%20v2_proof_results%5B_rid%5D%20%3D%20_vp(_script%2C%20v2_model_hash)%0A%0A%20%20%20%20_margin_rows%20%3D%20%22%5Cn%22.join(%0A%20%20%20%20%20%20%20%20f%22%7C%20%7Baxis%7D%20%7C%20%7Bval%3A.4f%7D%20%7C%20%7B'PASS'%20if%20val%20%3C%3D%20-0.010%20else%20'FAIL'%7D%20%7C%22%0A%20%20%20%20%20%20%20%20for%20axis%2C%20val%20in%20v2_margins.items()%0A%20%20%20%20)%0A%20%20%20%20_proof_rows%20%3D%20%22%5Cn%22.join(%0A%20%20%20%20%20%20%20%20f%22%7C%20%7Brid%7D%20%7C%20%7B'VERIFIED'%20if%20r.status%20%3D%3D%20_PS.VERIFIED%20else%20'FAILED'%7D%20%7C%22%0A%20%20%20%20%20%20%20%20for%20rid%2C%20r%20in%20sorted(v2_proof_results.items())%0A%20%20%20%20)%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Re-run%20Symbolic%20Analysis%20(Kp%3D4%2C%20Kd%3D30)%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22Inertia%20unchanged%3A%20Jxx%3D%7Bv2_sym.inertia%5B0%5D%3A.1f%7D%2C%20%22%0A%20%20%20%20%20%20%20%20f%22Jyy%3D%7Bv2_sym.inertia%5B1%5D%3A.1f%7D%2C%20Jzz%3D%7Bv2_sym.inertia%5B2%5D%3A.1f%7D%20kg.m%5E2%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**Stability%20margins%20(improved)%3A**%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Axis%20%7C%20Re(lambda)%20%7C%20Status%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C------%7C-----------%7C--------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7B_margin_rows%7D%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22Settling%20time%20estimate%3A%20**%7Bv2_sym.pointing_budget%5B'settling_time_s'%5D%3A.1f%7Ds**%20%22%0A%20%20%20%20%20%20%20%20f%22(was%20262s%2C%20requirement%20is%20120s)%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**Proofs%20(re-verified%20against%20new%20model%20hash)%3A**%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Requirement%20%7C%20Status%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C-------------%7C--------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7B_proof_rows%7D%22%0A%20%20%20%20)%0A%20%20%20%20return%20v2_params%2C%20v2_proofs%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20v2_params)%3A%0A%20%20%20%20from%20analysis.numerical%20import%20run_step_response%20as%20_rsr%0A%0A%20%20%20%20v2_step%20%3D%20_rsr(v2_params)%0A%20%20%20%20v2_step_summary%20%3D%20v2_step.summary()%0A%0A%20%20%20%20import%20matplotlib.pyplot%20as%20_plt2%0A%20%20%20%20import%20numpy%20as%20_np2%0A%0A%20%20%20%20_fig2%2C%20_ax2%20%3D%20_plt2.subplots(1%2C%202%2C%20figsize%3D(14%2C%205))%0A%20%20%20%20_axis_colors%20%3D%20%7B%22X%22%3A%20%22%231f77b4%22%2C%20%22Y%22%3A%20%22%232ca02c%22%2C%20%22Z%22%3A%20%22%239467bd%22%7D%0A%20%20%20%20_limit_color%20%3D%20%22%23d62728%22%0A%0A%20%20%20%20%23%20Pointing%20convergence%20comparison%0A%20%20%20%20_q_vec2%20%3D%20_np2.linalg.norm(v2_step.q%5B%3A%2C%20%3A3%5D%2C%20axis%3D1)%0A%20%20%20%20_theta2%20%3D%20_np2.degrees(2%20*%20_q_vec2)%0A%20%20%20%20_ax2%5B0%5D.semilogy(v2_step.t%2C%20_theta2%2C%20color%3D_axis_colors%5B%22X%22%5D%2C%20linewidth%3D1.5%2C%20label%3D%22Kp%3D4%2C%20Kd%3D30%20(updated)%22)%0A%20%20%20%20_ax2%5B0%5D.axhline(0.1%2C%20color%3D_limit_color%2C%20linestyle%3D%22--%22%2C%20linewidth%3D1%2C%20label%3D%22REQ-001%20limit%22)%0A%20%20%20%20_ax2%5B0%5D.axvline(120%2C%20color%3D%22%23888%22%2C%20linestyle%3D%22%3A%22%2C%20linewidth%3D1%2C%20alpha%3D0.7%2C%20label%3D%22120s%20target%22)%0A%20%20%20%20_ax2%5B0%5D.set_xlabel(%22Time%20(s)%22)%0A%20%20%20%20_ax2%5B0%5D.set_ylabel(%22Attitude%20Error%20(deg)%22)%0A%20%20%20%20_ax2%5B0%5D.set_title(%22Pointing%20Convergence%20(Kp%3D4%2C%20Kd%3D30)%22)%0A%20%20%20%20_ax2%5B0%5D.set_ylim(bottom%3D1e-4)%0A%20%20%20%20_ax2%5B0%5D.legend(fontsize%3D8)%0A%20%20%20%20_ax2%5B0%5D.grid(True%2C%20alpha%3D0.3%2C%20which%3D%22both%22)%0A%0A%20%20%20%20%23%20Wheel%20momentum%0A%20%20%20%20_h2%20%3D%20_np2.linalg.norm(v2_step.h_wheel%2C%20axis%3D1)%0A%20%20%20%20_ax2%5B1%5D.plot(v2_step.t%2C%20_h2%2C%20color%3D_axis_colors%5B%22X%22%5D%2C%20linewidth%3D1.5%2C%20label%3D%22%7Ch%7C%20(total)%22)%0A%20%20%20%20_ax2%5B1%5D.axhline(v2_step.config.max_momentum%2C%20color%3D_limit_color%2C%20linestyle%3D%22--%22%2C%20linewidth%3D1%2C%20label%3D%22REQ-002%20limit%22)%0A%20%20%20%20_ax2%5B1%5D.set_xlabel(%22Time%20(s)%22)%0A%20%20%20%20_ax2%5B1%5D.set_ylabel(%22Momentum%20(N.m.s)%22)%0A%20%20%20%20_ax2%5B1%5D.set_title(%22Wheel%20Momentum%20(Kp%3D4%2C%20Kd%3D30)%22)%0A%20%20%20%20_ax2%5B1%5D.legend(fontsize%3D8)%0A%20%20%20%20_ax2%5B1%5D.grid(True%2C%20alpha%3D0.3)%0A%0A%20%20%20%20_fig2.suptitle(%22Design%20Iteration%3A%20Step%20Response%20with%20Kp%3D4%2C%20Kd%3D30%22%2C%20fontsize%3D13%2C%20fontweight%3D%22bold%22)%0A%20%20%20%20_plt2.tight_layout()%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Re-run%20Numerical%20Simulation%20(Kp%3D4%2C%20Kd%3D30)%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Metric%20%7C%20Kd%3D10%20(original)%20%7C%20Kd%3D30%20(updated)%20%7C%20Requirement%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C--------%7C-----------------%7C-----------------%7C-------------%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Settling%20time%20%7C%20262s%20%7C%20**%7Bv2_step_summary%5B'settling_time_s'%5D%3A.1f%7Ds**%20%7C%20%3C%20120s%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Final%20error%20%7C%200.1223%20deg%20%7C%20**%7Bv2_step_summary%5B'final_error_deg'%5D%3A.4f%7D%20deg**%20%7C%20%3C%200.1%20deg%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Peak%20momentum%20%7C%200.810%20N.m.s%20%7C%20**%7Bv2_step_summary%5B'peak_wheel_momentum'%5D%3A.3f%7D%20N.m.s**%20%7C%20%3C%204.0%20N.m.s%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%7C%20Peak%20torque%20%7C%200.044%20N.m%20%7C%20**%7Bv2_step_summary%5B'peak_control_torque'%5D%3A.4f%7D%20N.m**%20%7C%20%3C%200.1%20N.m%20%7C%5Cn%22%0A%20%20%20%20)%0A%0A%20%20%20%20_fig2%0A%20%20%20%20return%20v2_step%2C%20v2_step_summary%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20%23%23%23%20Regression%20Check%0A%0A%20%20%20%20With%20Kp%3D4%2C%20Kd%3D30%2C%20the%20settling%20time%20is%20now%20well%20under%20120s.%20But%20we%20must%0A%20%20%20%20verify%20that%20the%20gain%20increase%20didn't%20break%20anything%20else%3A%0A%0A%20%20%20%20-%20**REQ-002%20(momentum)%3A**%20Peak%20momentum%20may%20increase%20(higher%20gains%20%E2%86%92%20more%0A%20%20%20%20%20%20aggressive%20control)%2C%20but%20must%20remain%20within%20the%204.0%20N.m.s%20limit.%0A%20%20%20%20-%20**REQ-003%20(stability)%3A**%20Higher%20gains%20improve%20both%20bandwidth%20and%20damping.%0A%20%20%20%20-%20**REQ-004%20(disturbance)%3A**%20Gravity%20gradient%20rejection%20improves%20%E2%80%94%20higher%20Kp%0A%20%20%20%20%20%20reduces%20steady-state%20error%20from%20disturbances.%0A%0A%20%20%20%20This%20is%20**reproducibility%20as%20regression%20testing**.%20The%20same%20pipeline%20that%20found%0A%20%20%20%20the%20deficiency%20now%20confirms%20the%20fix%20doesn't%20introduce%20new%20problems.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20v2_graph%2C%20v2_model_hash%2C%20v2_proofs%2C%20v2_step%2C%20v2_step_summary)%3A%0A%20%20%20%20from%20evidence.binding%20import%20(%0A%20%20%20%20%20%20%20%20bind_proof_evidence%20as%20_bpe%2C%20bind_simulation_evidence%20as%20_bse%2C%0A%20%20%20%20%20%20%20%20bind_computation_engines%20as%20_bce%2C%0A%20%20%20%20)%0A%20%20%20%20from%20evidence.hashing%20import%20(%0A%20%20%20%20%20%20%20%20hash_proof%20as%20_hp2%2C%20hash_evidence%20as%20_he2%2C%20hash_simulation%20as%20_hs2%2C%0A%20%20%20%20)%0A%20%20%20%20from%20pipeline.dataset%20import%20graph_for%20as%20_gf%0A%20%20%20%20from%20traceability.rtm%20import%20load_base_dataset%20as%20_lbd%0A%20%20%20%20from%20traceability.attestation%20import%20request_attestation%20as%20_ra%0A%0A%20%20%20%20%23%20Build%20v2%20RTM%20as%20a%20Dataset%20so%20the%20new%20audit%20module%20(Act%2010)%20can%0A%20%20%20%20%23%20query%20it%20with%20named-graph%20awareness.%20Replace%20the%20structural%20layer%0A%20%20%20%20%23%20with%20the%20v2%20model%20(Kp%3D4%2C%20Kd%3D30).%0A%20%20%20%20v2_rtm%20%3D%20_lbd()%0A%20%20%20%20_struct_v2%20%3D%20_gf(v2_rtm%2C%20%22structural%22)%0A%20%20%20%20%23%20Wipe%20the%20original%20structural%20triples%20and%20replace%20with%20v2_graph%0A%20%20%20%20for%20_t%20in%20list(_struct_v2)%3A%0A%20%20%20%20%20%20%20%20_struct_v2.remove(_t)%0A%20%20%20%20for%20_t%20in%20v2_graph%3A%0A%20%20%20%20%20%20%20%20_struct_v2.add(_t)%0A%0A%20%20%20%20_ev2%20%3D%20_gf(v2_rtm%2C%20%22evidence%22)%0A%20%20%20%20_bce(_ev2)%0A%0A%20%20%20%20for%20_rid%2C%20_script%20in%20v2_proofs.items()%3A%0A%20%20%20%20%20%20%20%20_ph%20%3D%20_hp2(_script%2C%20v2_model_hash)%0A%20%20%20%20%20%20%20%20_ch%20%3D%20_he2(v2_model_hash%2C%20proof_hash%3D_ph)%0A%20%20%20%20%20%20%20%20_bpe(_ev2%2C%20f%22EV-PROOF-%7B_rid%7D-v2%22%2C%20f%22SA-%7B_rid%7D-v2%22%2C%20_rid%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20v2_model_hash%2C%20_ph%2C%20_ch%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20f%22Symbolic%20proof%20(v2)%3A%20%7B_script.claim%7D%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20source_file%3D%22analysis%2Fbuild_proofs.py%22)%0A%0A%20%20%20%20_sh2%20%3D%20_hs2(v2_step.config.to_dict()%2C%20v2_step_summary)%0A%20%20%20%20for%20_rid%2C%20_desc%20in%20%5B%0A%20%20%20%20%20%20%20%20(%22REQ-001%22%2C%20f%22Step%20response%20(v2)%3A%20settling%3D%7Bv2_step_summary%5B'settling_time_s'%5D%3A.1f%7Ds%2C%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20f%22final_error%3D%7Bv2_step_summary%5B'final_error_deg'%5D%3A.4f%7D%20deg%22)%2C%0A%20%20%20%20%20%20%20%20(%22REQ-002%22%2C%20f%22Peak%20wheel%20momentum%20(v2)%3A%20%7Bv2_step_summary%5B'peak_wheel_momentum'%5D%3A.3f%7D%20N.m.s%22)%2C%0A%20%20%20%20%5D%3A%0A%20%20%20%20%20%20%20%20_bse(_ev2%2C%20f%22EV-SIM-%7B_rid%7D-v2%22%2C%20f%22NS-%7B_rid%7D-v2%22%2C%20_rid%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20%20v2_model_hash%2C%20_sh2%2C%20_desc%2C%20source_file%3D%22analysis%2Fnumerical.py%22)%0A%0A%20%20%20%20%23%20Attest%20ALL%204%20requirements%20with%20earl%3Apassed%20%E2%80%94%20the%20v2%20evidence%20is%0A%20%20%20%20%23%20now%20sufficient%20(settling%20time%20met).%0A%20%20%20%20_v2_adequacy%20%3D%20%7B%0A%20%20%20%20%20%20%20%20%22REQ-001%22%3A%20(%22Linearized%20PD%20model%20adequate.%20Kp%20increased%20to%204%2C%20Kd%20to%2030%20per%20design%20review%20finding.%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%22Interface%20parameters%20unchanged%20from%20systems%20engineering.%22)%2C%0A%20%20%20%20%20%20%20%20%22REQ-002%22%3A%20%22Energy-based%20momentum%20bound%20conservative.%20Peak%20may%20increase%20with%20higher%20gains%20but%20within%20limits.%22%2C%0A%20%20%20%20%20%20%20%20%22REQ-003%22%3A%20%22Routh-Hurwitz%20stability%20confirmed.%20Higher%20gains%20improve%20damping%20and%20bandwidth.%22%2C%0A%20%20%20%20%20%20%20%20%22REQ-004%22%3A%20%22GG%20model%20adequate.%20Controller%20gain%20change%20does%20not%20affect%20disturbance%20torque%20magnitude.%22%2C%0A%20%20%20%20%7D%0A%20%20%20%20_v2_sufficiency%20%3D%20%7B%0A%20%20%20%20%20%20%20%20%22REQ-001%22%3A%20(f%22Settling%20time%20now%20%7Bv2_step_summary%5B'settling_time_s'%5D%3A.1f%7Ds%20(%3C%20120s%20requirement).%20%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20f%22Pointing%20accuracy%20%7Bv2_step_summary%5B'final_error_deg'%5D%3A.4f%7D%20deg%20(%3C%200.1%20deg).%20Both%20met.%22)%2C%0A%20%20%20%20%20%20%20%20%22REQ-002%22%3A%20f%22Peak%20momentum%20%7Bv2_step_summary%5B'peak_wheel_momentum'%5D%3A.3f%7D%20N.m.s%2C%20well%20within%204.0%20limit.%22%2C%0A%20%20%20%20%20%20%20%20%22REQ-003%22%3A%20%22Routh-Hurwitz%20proof%20valid%20for%20all%20positive%20J%2C%20Kp%2C%20Kd.%20Margins%20improved%20with%20higher%20gains.%22%2C%0A%20%20%20%20%20%20%20%20%22REQ-004%22%3A%20%22GG%20torques%20unchanged%20at%20~1e-6%20N.m.%20Overwhelming%20margin%20vs%200.1%20N.m%20actuator%20capacity.%22%2C%0A%20%20%20%20%7D%0A%0A%20%20%20%20for%20_rid%20in%20%5B%22REQ-001%22%2C%20%22REQ-002%22%2C%20%22REQ-003%22%2C%20%22REQ-004%22%5D%3A%0A%20%20%20%20%20%20%20%20_ra(v2_rtm%2C%20_rid%2C%20%22Dr.%20Michael%20Zargham%20(%40mzargham)%22%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20auto_attest%3DTrue%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20model_adequacy%3D_v2_adequacy%5B_rid%5D%2C%0A%20%20%20%20%20%20%20%20%20%20%20%20evidence_sufficiency%3D_v2_sufficiency%5B_rid%5D)%0A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20%23%23%23%20Full%20Re-attestation%20(v2%20model)%0A%0A%20%20%20%20With%20the%20updated%20model%2C%20all%20four%20requirements%20now%20have%20sufficient%20evidence%3A%0A%0A%20%20%20%20-%20**REQ-001%3A%20ATTESTED**%20%E2%80%94%20settling%20time%20and%20pointing%20accuracy%20both%20met%0A%20%20%20%20-%20**REQ-002%3A%20ATTESTED**%20%E2%80%94%20momentum%20within%20limits%20(slight%20increase%20noted)%0A%20%20%20%20-%20**REQ-003%3A%20ATTESTED**%20%E2%80%94%20stability%20margins%20improved%0A%20%20%20%20-%20**REQ-004%3A%20ATTESTED**%20%E2%80%94%20disturbance%20rejection%20unchanged%0A%0A%20%20%20%20The%20entire%20evidence%20chain%20is%20fresh%20%E2%80%94%20new%20model%20hash%2C%20new%20proof%20hashes%2C%0A%20%20%20%20new%20simulation%20hashes.%20Nothing%20carries%20over%20from%20the%20v1%20analysis.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%20(v2_rtm%2C)%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(v2_rtm)%3A%0A%20%20%20%20from%20interrogate.visualize%20import%20build_rtm_figure%20as%20_brf%0A%0A%20%20%20%20v2_fig%20%3D%20_brf(v2_rtm%2C%20figsize%3D(18%2C%2010)%2C%20title%3D%22Requirements%20Traceability%20Matrix%20(v2%3A%20Kp%3D4%2C%20Kd%3D30)%22)%0A%20%20%20%20v2_fig%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20v2_rtm)%3A%0A%20%20%20%20from%20interrogate.explain%20import%20explain_requirement%20as%20_er%0A%0A%20%20%20%20_v2_expl%20%3D%20_er(v2_rtm%2C%20%22REQ-001%22)%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20'%23%23%23%20%22How%20do%20you%20know%20REQ-001%20is%20satisfied%20now%3F%22%5Cn%5Cn'%0A%20%20%20%20%20%20%20%20f%22%60%60%60%5Cn%7B_v2_expl%7D%5Cn%60%60%60%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22The%20traceability%20chain%20is%20now%20**complete**%20for%20REQ-001.%20The%20auditor%20can%20see%3A%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22-%20Fresh%20proof%20artifact%20bound%20to%20the%20v2%20model%20hash%5Cn%22%0A%20%20%20%20%20%20%20%20%22-%20Fresh%20simulation%20showing%20settling%20time%20under%20120s%5Cn%22%0A%20%20%20%20%20%20%20%20%22-%20Attestation%20by%20Dr.%20Zargham%20with%20explicit%20reference%20to%20the%20design%20change%5Cn%22%0A%20%20%20%20%20%20%20%20%22-%20The%20v2%20model%20hash%20differs%20from%20v1%20%E2%80%94%20confirming%20this%20is%20new%20evidence%2C%20not%20recycled%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%209%3A%20Remote%20Compute%20%26%20Distribution%0A%0A%20%20%20%20Up%20to%20now%20the%20analysis%20ran%20on%20the%20engineer's%20local%20machine.%20In%0A%20%20%20%20production%20aerospace%20deployments%2C%20the%20**compute%20server**%20is%20usually%20a%0A%20%20%20%20different%20physical%20host%20than%20where%20the%20engineer%20reviews%20results%20%E2%80%94%20a%0A%20%20%20%20remote%20analysis%20cluster%2C%20a%20CI%20runner%2C%20or%20a%20containerized%20environment%0A%20%20%20%20pinned%20to%20a%20known%20toolchain.%20The%20RTM%20must%20record%20*where*%20and%20*how*%0A%20%20%20%20each%20piece%20of%20evidence%20was%20produced%2C%20otherwise%20the%20audit%20chain%20has%0A%20%20%20%20a%20gap.%0A%0A%20%20%20%20Two%20pluggable%20extensions%3A%0A%0A%20%20%20%201.%20**Compute%20backends**%20%E2%80%94%20%60LocalCompute%60%20(default%2C%20in-process)%20or%0A%20%20%20%20%20%20%20%60DockerCompute%60%20(ephemeral%20container%20per%20analysis%20stage).%20The%0A%20%20%20%20%20%20%20container's%20identity%20(image%20digest%2C%20container%20ID%2C%20hostname)%20is%0A%20%20%20%20%20%20%20captured%20as%20PROV-O%20triples%20on%20the%20analysis%20activity.%0A%20%20%20%202.%20**Persistence%20backends**%20%E2%80%94%20%60LocalBackend%60%20(filesystem)%20or%0A%20%20%20%20%20%20%20%60FlexoBackend%60%20%2F%20%60FuskeiBackend%60%20(a%20real%20quadstore).%20Each%20named%0A%20%20%20%20%20%20%20graph%20in%20our%20%60rdflib.Dataset%60%20maps%20to%20a%20Flexo%20branch.%0A%0A%20%20%20%20For%20this%20notebook%20we%20annotate%20v2's%20analysis%20activities%20*as%20if*%20they%0A%20%20%20%20had%20run%20inside%20an%20%60adcs-compute%3Alatest%60%20container%20%E2%80%94%20so%20the%20auditor%0A%20%20%20%20can%20see%20the%20captured%20execution%20context%20in%20Act%2010.%20In%20a%20live%20run%0A%20%20%20%20%60--compute%3Ddocker%60%20does%20the%20actual%20container%20spawn%20and%20captures%0A%20%20%20%20real%20digests.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20v2_rtm)%3A%0A%20%20%20%20from%20compute.base%20import%20ExecutionMetadata%20as%20_ExecMeta%0A%20%20%20%20from%20evidence.binding%20import%20_bind_execution_metadata%20as%20_bind_meta%0A%20%20%20%20from%20ontology.prefixes%20import%20ADCS%20as%20_ADCS%2C%20G_EVIDENCE%20as%20_G_EV%0A%20%20%20%20from%20rdflib%20import%20URIRef%20as%20_URI%0A%0A%20%20%20%20%23%20Simulate%20captured%20metadata%20from%20a%20Docker%20compute%20run.%20In%20a%20live%0A%20%20%20%20%23%20pipeline%20(%60--compute%3Ddocker%60)%20these%20values%20come%20from%20the%20real%0A%20%20%20%20%23%20%60docker%20image%20inspect%60%20%2B%20container%20hostname%20%2B%20cidfile.%0A%20%20%20%20_exec_meta%20%3D%20_ExecMeta(%0A%20%20%20%20%20%20%20%20location_kind%3D%22docker%22%2C%0A%20%20%20%20%20%20%20%20hostname%3D%22container-71a59f23f3e9%22%2C%0A%20%20%20%20%20%20%20%20image_digest%3D%22sha256%3A92bb8bf18f5f2ba7a6e332e4fe1fa1b12911e9b6c4cddb4b35e1659b01b21d30%22%2C%0A%20%20%20%20%20%20%20%20image_label%3D%22adcs-compute%3Alatest%22%2C%0A%20%20%20%20%20%20%20%20container_id%3D%2271a59f23f3e9%22%2C%0A%20%20%20%20%20%20%20%20python_version%3D%223.12.13%22%2C%0A%20%20%20%20%20%20%20%20started_at%3D%222026-05-14T02%3A27%3A51%2B00%3A00%22%2C%0A%20%20%20%20%20%20%20%20ended_at%3D%222026-05-14T02%3A27%3A56%2B00%3A00%22%2C%0A%20%20%20%20)%0A%0A%20%20%20%20_ev_g%20%3D%20v2_rtm.graph(_URI(_G_EV))%0A%20%20%20%20for%20_rid%20in%20%5B%22REQ-001%22%2C%20%22REQ-002%22%2C%20%22REQ-003%22%2C%20%22REQ-004%22%5D%3A%0A%20%20%20%20%20%20%20%20_bind_meta(_ev_g%2C%20_ADCS%5Bf%22SA-%7B_rid%7D-v2%22%5D%2C%20_exec_meta)%0A%20%20%20%20%20%20%20%20_bind_meta(_ev_g%2C%20_ADCS%5Bf%22NS-%7B_rid%7D-v2%22%5D%2C%20_exec_meta)%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20Remote-compute%20provenance%20attached%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22Each%20v2%20analysis%20activity%20(%60SA-*-v2%60%2C%20%60NS-*-v2%60)%20now%20carries%3A%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60turtle%5Cn%22%0A%20%20%20%20%20%20%20%20%22adcs%3ASA-REQ-003-v2%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20prov%3AatLocation%20%20%20%20%20%20%20%20%3Curn%3Aadcs%3Alocation%3Adocker%3Acontainer-71a59f23f3e9%3E%20%3B%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20prov%3AwasAssociatedWith%20%3Curn%3Aadcs%3Aexecutor%3A71a59f23f3e9%3E%20%3B%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20prov%3AstartedAtTime%20%20%20%20%20%5C%222026-05-14T02%3A27%3A51%2B00%3A00%5C%22%5E%5Exsd%3AdateTime%20%3B%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20prov%3AendedAtTime%20%20%20%20%20%20%20%5C%222026-05-14T02%3A27%3A56%2B00%3A00%5C%22%5E%5Exsd%3AdateTime%20.%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%3Curn%3Aadcs%3Aexecutor%3A71a59f23f3e9%3E%20a%20prov%3ASoftwareAgent%20%3B%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20rtm%3Ahostname%20%20%20%20%20%20%5C%22container-71a59f23f3e9%5C%22%20%3B%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20rtm%3AimageDigest%20%20%20%5C%22sha256%3A92bb8bf18f5f...%5C%22%20%3B%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20rtm%3AimageLabel%20%20%20%20%5C%22adcs-compute%3Alatest%5C%22%20%3B%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20rtm%3AcontainerId%20%20%20%5C%2271a59f23f3e9%5C%22%20%3B%5Cn%22%0A%20%20%20%20%20%20%20%20%22%20%20%20%20rtm%3ApythonVersion%20%5C%223.12.13%5C%22%20.%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22The%20image%20digest%20pins%20the%20toolchain%20version%20cryptographically.%20%22%0A%20%20%20%20%20%20%20%20%22If%20someone%20replays%20the%20analysis%2C%20they%20pull%20the%20same%20image%20by%20%22%0A%20%20%20%20%20%20%20%20%22digest%20and%20get%20an%20identical%20environment%20%E2%80%94%20not%20'a%20Python%20with%20%22%0A%20%20%20%20%20%20%20%20%22scipy%20somewhere'%20but%20*that*%20Python%20with%20*that*%20scipy.%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**Distribution**%20is%20the%20parallel%20story%20for%20persistence.%20The%20same%20%22%0A%20%20%20%20%20%20%20%20%22v2_rtm%20Dataset%20can%20be%20pushed%20to%20a%20real%20quadstore%3A%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60bash%5Cn%22%0A%20%20%20%20%20%20%20%20%22export%20FLEXO_TOKEN%3D...%20%20%20%20%20%23%20from%20a%20collaborator%20on%20the%20sandbox%5Cn%22%0A%20%20%20%20%20%20%20%20%22make%20flexo-init%20%20%20%20%20%20%20%20%20%20%20%20%20%23%20one-time%3A%20provision%20org%20%2F%20repo%20%2F%20master%5Cn%22%0A%20%20%20%20%20%20%20%20%22make%20flexo-run%20%20%20%20%20%20%20%20%20%20%20%20%20%20%23%20%3D%20pipeline.runner%20--backend%3Dflexo%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22Live%20result%20against%20%60try-layer1.starforge.app%60%3A%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Branch%20%7C%20Triples%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C---%7C---%3A%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20ontology%20%7C%20317%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20structural%20%7C%20253%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20evidence%20%7C%20126%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20attestations%20%7C%2089%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20plan-execution%20%7C%2052%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20audit%20%7C%208%20%7C%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60SPARQL%20ASK%20%7B%20adcs%3AATT-REQ-003%20a%20rtm%3AAttestation%20%7D%60%20returns%20%22%0A%20%20%20%20%20%20%20%20%22%60true%60%20on%20the%20attestations%20branch%20%E2%80%94%20the%20data%20is%20queryable%20end-%22%0A%20%20%20%20%20%20%20%20%22to-end%20from%20a%20host%20the%20engineer%20never%20logged%20into.%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Act%2010%3A%20Fresh%20Audit%20(after%20remote%20compute)%0A%0A%20%20%20%20The%20audit%20module%20is%20**backend-agnostic**%20and%20**compute-agnostic**%20%E2%80%94%0A%20%20%20%20it%20queries%20the%20local%20Dataset%20whether%20the%20analysis%20ran%20in-process%20or%0A%20%20%20%20in%20a%20container%2C%20whether%20the%20persistence%20lands%20on%20disk%20or%20in%20Flexo.%0A%20%20%20%20What%20the%20auditor%20gets%2C%20after%20Act%209's%20annotations%2C%20is%20a%20richer%20trace%0A%20%20%20%20that%20includes%20the%20execution%20context%20per%20activity.%0A%0A%20%20%20%20We%20re-run%20the%20audit%20against%20the%20v2%20Dataset%20and%20surface%20two%20things%0A%20%20%20%20the%20original%20audit%20(Act%206)%20couldn't%20show%3A%0A%0A%20%20%20%201.%20The%20complete%20forward%20%2F%20backward%20%2F%20bidirectional%20verdict%20on%20v2%0A%20%20%20%20%20%20%20(now%20that%20REQ-001%20passes%20too).%0A%20%20%20%202.%20The%20execution-context%20triples%20%E2%80%94%20a%20SPARQL%20query%20that%20answers%0A%20%20%20%20%20%20%20*%22Where%20and%20on%20what%20image%20was%20each%20piece%20of%20v2%20evidence%0A%20%20%20%20%20%20%20produced%3F%22*%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20v2_rtm)%3A%0A%20%20%20%20from%20traceability.audit%20import%20audit%20as%20_audit_fn_v2%0A%0A%20%20%20%20_v2_audit%20%3D%20_audit_fn_v2(v2_rtm)%0A%20%20%20%20_rows%20%3D%20%22%5Cn%22.join(%0A%20%20%20%20%20%20%20%20f%22%7C%20%7Bc.requirement%7D%20%7C%20%7Bc.evidence%7D%20%7C%20%7Bc.status%7D%20%7C%22%0A%20%20%20%20%20%20%20%20for%20c%20in%20_v2_audit.coverage%0A%20%20%20%20)%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20%22%23%23%23%20v2%20audit%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%20%20%20%20%7B_v2_audit.forward.summary()%7D%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%20%20%20%20%7B_v2_audit.backward.summary()%7D%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%20%20%20%20Bidirectional%3A%20%7B'PASS'%20if%20_v2_audit.bidirectional().passed%20else%20'FAIL'%7D%5Cn%22%0A%20%20%20%20%20%20%20%20f%22%20%20%20%20Orphans%3A%20%7B'none'%20if%20not%20_v2_audit.orphans.any%20else%20'see%20report'%7D%5Cn%22%0A%20%20%20%20%20%20%20%20%22%60%60%60%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22**Coverage%20matrix%20(v2)%3A**%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C%20Requirement%20%7C%20Evidence%20%7C%20Status%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%22%7C---%7C---%7C---%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%2B%20_rows%20%2B%20%22%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22Every%20requirement%20now%20shows%20%60covered%2Bpassed%60.%20The%20same%20audit%20%22%0A%20%20%20%20%20%20%20%20%22code%20that%20flagged%20REQ-001%20as%20%60covered%2Bfailed%60%20in%20Act%206%20here%20%22%0A%20%20%20%20%20%20%20%20%22reports%20it%20as%20resolved%20%E2%80%94%20and%20the%20closure-rule%20suite%2C%20%22%0A%20%20%20%20%20%20%20%20%22explanation%20chain%2C%20and%20re-verification%20all%20continue%20to%20pass%20%22%0A%20%20%20%20%20%20%20%20%22(the%20design%20iteration%20didn't%20break%20anything%20else).%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo%2C%20v2_rtm)%3A%0A%20%20%20%20%23%20SPARQL%20across%20the%20union%20to%20pull%20each%20analysis%20activity's%20execution%0A%20%20%20%20%23%20context.%20default_union%20makes%20this%20work%20without%20explicit%20GRAPH%0A%20%20%20%20%23%20clauses%20%E2%80%94%20see%20Prologue.%0A%20%20%20%20_q%20%3D%20%22%22%22%0A%20%20%20%20PREFIX%20prov%3A%20%3Chttp%3A%2F%2Fwww.w3.org%2Fns%2Fprov%23%3E%0A%20%20%20%20PREFIX%20rtm%3A%20%20%3Chttp%3A%2F%2Fexample.org%2Fontology%2Frtm%23%3E%0A%20%20%20%20SELECT%20%3Factivity%20%3Flocation%20%3Fimage%20%3Fhost%20%3Fstarted%20WHERE%20%7B%0A%20%20%20%20%20%20%20%20%3Factivity%20prov%3AatLocation%20%3Flocation%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20prov%3AwasAssociatedWith%20%3Fexecutor%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20prov%3AstartedAtTime%20%3Fstarted%20.%0A%20%20%20%20%20%20%20%20%3Fexecutor%20a%20prov%3ASoftwareAgent%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20rtm%3AimageLabel%20%3Fimage%20%3B%0A%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20%20rtm%3Ahostname%20%3Fhost%20.%0A%20%20%20%20%7D%0A%20%20%20%20ORDER%20BY%20%3Factivity%0A%20%20%20%20%22%22%22%0A%20%20%20%20_rows%20%3D%20%5B%5D%0A%20%20%20%20for%20r%20in%20v2_rtm.query(_q)%3A%0A%20%20%20%20%20%20%20%20_act%20%3D%20str(r.activity).rsplit(%22%2F%22%2C%201)%5B-1%5D%0A%20%20%20%20%20%20%20%20_img%20%3D%20str(r.image)%0A%20%20%20%20%20%20%20%20_host%20%3D%20str(r.host)%0A%20%20%20%20%20%20%20%20_rows.append(f%22%7C%20%7B_act%7D%20%7C%20%7B_img%7D%20%7C%20%7B_host%7D%20%7C%22)%0A%0A%20%20%20%20if%20not%20_rows%3A%0A%20%20%20%20%20%20%20%20_body%20%3D%20%22_no%20execution-context%20triples%20found_%22%0A%20%20%20%20else%3A%0A%20%20%20%20%20%20%20%20_body%20%3D%20(%0A%20%20%20%20%20%20%20%20%20%20%20%20%22%7C%20Activity%20%7C%20Image%20%7C%20Host%20%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%22%7C---%7C---%7C---%7C%5Cn%22%0A%20%20%20%20%20%20%20%20%20%20%20%20%2B%20%22%5Cn%22.join(_rows)%0A%20%20%20%20%20%20%20%20)%0A%0A%20%20%20%20mo.md(%0A%20%20%20%20%20%20%20%20'%23%23%23%20%22Where%20and%20on%20what%20image%20was%20each%20v2%20piece%20of%20evidence%20produced%3F%22%5Cn%5Cn'%0A%20%20%20%20%20%20%20%20f%22%7B_body%7D%5Cn%5Cn%22%0A%20%20%20%20%20%20%20%20%22The%20audit%20chain%20now%20goes%20all%20the%20way%20to%20the%20executor.%20An%20auditor%20%22%0A%20%20%20%20%20%20%20%20%22reviewing%20this%20RTM%20can%20pull%20the%20exact%20image%20by%20digest%2C%20replay%20%22%0A%20%20%20%20%20%20%20%20%22the%20analysis%2C%20and%20verify%20the%20proofs%20re-derive%20bit-for-bit%20%E2%80%94%20%22%0A%20%20%20%20%20%20%20%20%22without%20trusting%20the%20engineer's%20local%20environment.%22%0A%20%20%20%20)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Future%20Work%0A%0A%20%20%20%20The%20demo%20deliberately%20stops%20short%20of%20several%20production-grade%0A%20%20%20%20extensions%2C%20each%20documented%20in%0A%20%20%20%20%5B%60%2FUsers%2Fz%2F.claude%2Fplans%2Fi-want-to-look-hidden-balloon.md%60%5D(%23)%20and%0A%20%20%20%20summarized%20below%3A%0A%0A%20%20%20%20-%20**Cryptographic%20envelopes%20%26%20signatures.**%20Today%20hashes%20are%20bare%0A%20%20%20%20%20%20SHA-256%3A%20content%20identity%2C%20but%20not%20authenticity.%20Production%0A%20%20%20%20%20%20should%20layer%20W3C%20VC%20Data%20Integrity%20(Ed25519%20over%20RDF%0A%20%20%20%20%20%20canonicalization)%2C%20in-toto%2FSLSA%20build%20attestations%2C%20and%0A%20%20%20%20%20%20sigstore%2FRekor%20transparency%20logs.%0A%20%20%20%20-%20**Formal%20authority%20%26%20credential%20model.**%20FOAF%20%2B%20W3C%20Org%20Ontology%20%2B%0A%20%20%20%20%20%20%60schema%3AhasCredential%60%20%2B%20W3C%20Verifiable%20Credentials%20on%20top%20of%0A%20%20%20%20%20%20%60prov%3AAgent%60%20%E2%80%94%20so%20an%20attestation%20can%20carry%20not%20just%20*who*%0A%20%20%20%20%20%20attested%20but%20*what%20role%20they%20were%20authorized%20in*%20and%20*what%0A%20%20%20%20%20%20credentials%20backed%20that%20authorization*.%0A%20%20%20%20-%20**OntoGSN%20confidence%20arguments.**%20Reify%20confidence%20in%20each%0A%20%20%20%20%20%20Assumption%20%2F%20Justification%20node%20so%20stakeholders%20can%20ask%20%22how%0A%20%20%20%20%20%20confident%20are%20you%20in%20your%20adequacy%20claim%3F%22%20as%20a%20queryable%20graph%0A%20%20%20%20%20%20instead%20of%20prose.%0A%20%20%20%20-%20**Defeaters%20%26%20revocation.**%20SACM%2FOntoGSN-style%20invalidation%20of%0A%20%20%20%20%20%20attestations%20when%20later%20evidence%20contradicts%20an%20earlier%0A%20%20%20%20%20%20assumption%20(e.g.%2C%20test-flight%20data%20invalidates%20a%20linearization%0A%20%20%20%20%20%20regime%20assumption).%0A%20%20%20%20-%20**Multi-attestation%20aggregation.**%20Sign-off%20policies%20(Engineering%0A%20%20%20%20%20%20%2B%20QA%20%2B%20Certifier%20must%20all%20attest%20with%20%60earl%3Apassed%60)%20expressed%0A%20%20%20%20%20%20as%20SHACL%20gates%20on%20requirement%20transitions.%0A%20%20%20%20-%20**Production%20Flexo%20deployment.**%20Multi-user%20auth%20(SSO)%2C%0A%20%20%20%20%20%20PR-style%20branches%20for%20RTM%20evolution%2C%20CI%20hooks%2C%20federation%20across%0A%20%20%20%20%20%20program-level%20Flexo%20instances.%0A%20%20%20%20-%20**OSLC%20connector**%20for%20DOORS%20Next%20%2F%20Jama%20%2F%20RQM.%0A%20%20%20%20-%20**Federated%20SPARQL**%20for%20cross-program%20traceability.%0A%20%20%20%20-%20**Continuous%20re-verification%20in%20CI**%20and%20a%20**live%20traceability%0A%20%20%20%20%20%20dashboard**%20%E2%80%94%20both%20compose%20with%20the%20cryptographic-envelope%20work.%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_(mo)%3A%0A%20%20%20%20mo.md(%22%22%22%0A%20%20%20%20---%0A%0A%20%20%20%20%23%23%20Summary%0A%0A%20%20%20%20The%20complete%20ADCS%20verification%20lifecycle%2C%20numbered%20to%20the%20Acts%20so%20it%0A%20%20%20%20doubles%20as%20a%20table%20of%20contents.%20Sub-indexes%20(a%2Fb%2Fc)%20call%20out%0A%20%20%20%20multiple%20distinct%20actions%20inside%20one%20Act.%0A%0A%20%20%20%20**Prologue.**%20Assembled%20the%20integration%20ontology%20from%20PROV-O%20%2B%20EARL%0A%20%20%20%20%2B%20OntoGSN%20%2B%20P-PLAN%20%2B%20OSLC%20RM%2FQM%20%2B%20the%20openCAESAR%20SysMLv2%20OWL%0A%20%20%20%20rendering.%20No%20novel%20epistemic%20vocabulary%20in%20%60rtm%3A%60%20%E2%80%94%20adequacy%20and%0A%20%20%20%20sufficiency%20are%20%60gsn%3AAssumption%60%20%2F%20%60gsn%3AJustification%60%20per%20the%0A%20%20%20%20Hawkins%E2%80%93Habli%20ACP%20categorization.%0A%0A%20%20%20%201.%20**The%20Assignment**%20%E2%80%94%0A%20%20%20%20%20%20%20a.%20received%20four%20requirements%20from%20systems%20engineering%2C%0A%20%20%20%20%20%20%20%20%20%20allocated%20to%20the%20ADCS%20subsystem%3B%0A%20%20%20%20%20%20%20b.%20loaded%20the%20structural%20model%20(SysMLv2%20RDF)%20into%0A%20%20%20%20%20%20%20%20%20%20%60%3Cadcs%3Astructural%3E%60.%0A%20%20%20%202.%20**Symbolic%20Analysis**%20%E2%80%94%20SymPy%20derived%2013%20lemmas%20across%204%20proof%0A%20%20%20%20%20%20%20scripts%20(inertia%20tensor%2C%20stability%20margins%2C%20pointing%20budget%2C%0A%20%20%20%20%20%20%20gravity-gradient%20bound%2C%20wheel-momentum%20bound).%20Each%20lemma%20is%0A%20%20%20%20%20%20%20independently%20re-verifiable%3B%20the%20proof%20hash%20binds%20the%20script%20to%0A%20%20%20%20%20%20%20a%20specific%20model%20hash.%0A%20%20%20%203.%20**Numerical%20Simulation**%20%E2%80%94%20scipy%20integrated%20quaternion%20%2B%20Euler%0A%20%20%20%20%20%20%20dynamics%20under%20the%20PD%20controller.%20The%20step%20response%20revealed%0A%20%20%20%20%20%20%20settling%20time%20%E2%89%88%20262s%2C%20exceeding%20the%20120s%20spec%20for%20REQ-001%20%E2%80%94%20the%0A%20%20%20%20%20%20%20v1%20engineering%20finding.%0A%20%20%20%204.%20**Evidence%20Binding**%20%E2%80%94%20emitted%204%20proof%20artifacts%20%2B%203%20simulation%0A%20%20%20%20%20%20%20results%20into%20%60%3Cadcs%3Aevidence%3E%60%2C%20each%20with%20content%20%2F%20model%20%2F%20proof%0A%20%20%20%20%20%20%20hashes%20and%20PROV-O%20provenance.%0A%20%20%20%205.%20**Attestation%20(GSN%20%2B%20EARL)**%20%E2%80%94%20emitted%20four%20well-formed%0A%20%20%20%20%20%20%20attestations%20into%20%60%3Cadcs%3Aattestations%3E%60%2C%20each%20with%20an%20adequacy%0A%20%20%20%20%20%20%20%60gsn%3AAssumption%60%2C%20a%20sufficiency%20%60gsn%3AJustification%60%2C%20an%20EARL%0A%20%20%20%20%20%20%20outcome%2C%20and%20a%20%60prov%3AqualifiedAssociation%60.%20REQ-001%20carries%0A%20%20%20%20%20%20%20%60earl%3Afailed%60%20rather%20than%20being%20silently%20omitted%2C%20keeping%20the%0A%20%20%20%20%20%20%20audit%20graph%20complete.%0A%20%20%20%206.%20**Closure-Rule%20Validation%20%2B%20Audit%20(initial)**%20%E2%80%94%0A%20%20%20%20%20%20%20a.%20ran%20the%20closure-rule%20suite%20(9%20SHACL%20shapes%20%2B%201%20runtime%0A%20%20%20%20%20%20%20%20%20%20re-verification)%20against%20%60rtm_graph%60%20%E2%80%94%20all%20pass%3B%0A%20%20%20%20%20%20%20b.%20ran%20the%20audit%20module%20%E2%80%94%20traceability%20is%20structurally%20intact%0A%20%20%20%20%20%20%20%20%20%20(forward%20%2F%20backward%20%2F%20bidirectional%20all%20PASS)%3B%20the%20coverage%0A%20%20%20%20%20%20%20%20%20%20matrix%20shows%20REQ-001%20%3D%20%60covered%2Bfailed%60%20(the%20expected%20v1%0A%20%20%20%20%20%20%20%20%20%20state%20%E2%80%94%20engineering%20finding%2C%20*not*%20a%20trace%20gap).%0A%20%20%20%207.%20**Traceability%20Graph**%20%E2%80%94%20rendered%20the%20v1%20RTM.%20Three%20green%0A%20%20%20%20%20%20%20attestation%20nodes%20(REQ-002%20%2F%203%20%2F%204%20%3D%20%60earl%3Apassed%60)%2C%20one%20red%0A%20%20%20%20%20%20%20(REQ-001%20%3D%20%60earl%3Afailed%60).%20Design%20elements%20in%20purple%20to%20keep%0A%20%20%20%20%20%20%20green%20%2F%20red%20reserved%20for%20the%20engineering%20verdict.%0A%20%20%20%208.%20**Design%20Iteration**%20%E2%80%94%0A%20%20%20%20%20%20%20a.%20applied%20a%20SPARQL%20UPDATE%20to%20retune%20both%20gains%20(Kp%3A%201%20%E2%86%92%204%2C%0A%20%20%20%20%20%20%20%20%20%20Kd%3A%2010%20%E2%86%92%2030)%20directly%20on%20the%20structural%20model%3B%0A%20%20%20%20%20%20%20b.%20model%20hash%20invalidated%20%E2%80%94%20re-ran%20symbolic%20%2B%20numerical%0A%20%20%20%20%20%20%20%20%20%20analysis%2C%20regenerated%20every%20proof%20and%20simulation%20hash%20from%0A%20%20%20%20%20%20%20%20%20%20scratch%20(no%20stale%20evidence%20carries%20over)%3B%0A%20%20%20%20%20%20%20c.%20re-attested%20all%20four%20requirements%20as%20%60earl%3Apassed%60%20against%0A%20%20%20%20%20%20%20%20%20%20the%20v2%20model.%0A%20%20%20%209.%20**Remote%20Compute%20%26%20Distribution**%20%E2%80%94%0A%20%20%20%20%20%20%20a.%20attached%20%60ExecutionMetadata%60%20(image%20digest%2C%20container%20ID%2C%0A%20%20%20%20%20%20%20%20%20%20hostname%2C%20Python%20version)%20to%20v2%20analysis%20activities%2C%0A%20%20%20%20%20%20%20%20%20%20emulating%20analysis%20run%20on%20a%20remote%20%60adcs-compute%3Alatest%60%0A%20%20%20%20%20%20%20%20%20%20container%3B%0A%20%20%20%20%20%20%20b.%20validated%20live%20persistence%20to%20Flexo%20MMS%20on%20the%20shared%0A%20%20%20%20%20%20%20%20%20%20%60try-layer1.starforge.app%60%20sandbox%20%E2%80%94%20each%20named%20graph%20lands%0A%20%20%20%20%20%20%20%20%20%20as%20its%20own%20branch%20under%20%60adcs-demo%2Flifecycle%60.%0A%20%20%20%2010.%20**Fresh%20Audit%20(after%20remote%20compute)**%20%E2%80%94%20re-ran%20audit%20%2B%20closure%0A%20%20%20%20%20%20%20%20rules%20against%20the%20v2%20Dataset.%20Coverage%20matrix%20is%20now%20all%0A%20%20%20%20%20%20%20%20%60covered%2Bpassed%60.%20A%20SPARQL%20query%20against%20the%20union%20view%20pulls%0A%20%20%20%20%20%20%20%20per-activity%20*where%20%26%20on%20what%20image%20was%20this%20produced*%20%E2%80%94%20the%0A%20%20%20%20%20%20%20%20audit%20chain%20now%20extends%20all%20the%20way%20to%20the%20executor.%0A%0A%20%20%20%20%23%23%23%20What%20makes%20this%20different%0A%0A%20%20%20%20-%20**Evidence%20is%20not%20verification.**%20Only%20human%20attestation%20closes%0A%20%20%20%20%20%20the%20loop%20%E2%80%94%20and%20attestation%20outcomes%20can%20be%20%60earl%3Afailed%60%2C%0A%20%20%20%20%20%20%60earl%3AcantTell%60%2C%20etc.%20The%20graph%20records%20the%20engineering%20verdict%2C%0A%20%20%20%20%20%20not%20a%20binary%20pass%2Ffail.%0A%20%20%20%20-%20**Failures%20are%20first-class.**%20REQ-001%20at%20v1%20is%20%60covered%2Bfailed%60%2C%0A%20%20%20%20%20%20not%20omitted.%20The%20audit%20trail%20is%20complete%20*because*%20the%20failure%0A%20%20%20%20%20%20is%20recorded.%0A%20%20%20%20-%20**Trace%20%E2%89%A0%20verdict.**%20Forward%2Fbackward%20traceability%20is%20a%0A%20%20%20%20%20%20structural%20property%20of%20the%20graph.%20Coverage%20status%20is%20an%0A%20%20%20%20%20%20engineering%20verdict%20per%20requirement.%20Act%206%20calls%20these%20out%20as%0A%20%20%20%20%20%20two%20orthogonal%20questions%3B%20the%20demo%20design%20relies%20on%20the%0A%20%20%20%20%20%20distinction.%0A%20%20%20%20-%20**Reproducibility%20is%20regression%20testing.**%20The%20pipeline%20that%0A%20%20%20%20%20%20found%20the%20deficiency%20at%20v1%20confirmed%20the%20fix%20didn't%20break%0A%20%20%20%20%20%20anything%20else%20at%20v2.%0A%20%20%20%20-%20**Model%20changes%20invalidate%20evidence.**%20Gain%20retune%20%E2%86%92%20model%20hash%0A%20%20%20%20%20%20changes%20%E2%86%92%20every%20dependent%20hash%20changes.%20No%20stale%20proofs%20survive%0A%20%20%20%20%20%20a%20structural-model%20edit.%0A%20%20%20%20-%20**Where%20matters%20as%20much%20as%20what.**%20Provenance%20captures%20not%20just%0A%20%20%20%20%20%20*what%20was%20computed*%20but%20*where%20and%20on%20what%20toolchain*%20(image%0A%20%20%20%20%20%20digest%20%2B%20container%20ID%20%2B%20hostname)%2C%20so%20a%20regulator%20can%20replay%0A%20%20%20%20%20%20the%20analysis%20against%20the%20same%20pinned%20environment.%0A%20%20%20%20-%20**Everything%20is%20in%20git%2C%20and%20everything%20composes.**%20Both%20model%0A%20%20%20%20%20%20versions%2C%20both%20evidence%20sets%2C%20both%20attestation%20records%20%E2%80%94%20all%0A%20%20%20%20%20%20text%2C%20all%20versioned.%20The%20same%20Dataset%20persists%20to%20disk%0A%20%20%20%20%20%20(%60--backend%3Dlocal%60)%2C%20to%20Flexo%20MMS%20(%60--backend%3Dflexo%60)%2C%20or%20to%0A%20%20%20%20%20%20Fuseki%20(%60--backend%3Dfuseki%60)%20without%20changing%20a%20SPARQL%20query.%0A%0A%20%20%20%20%23%23%23%20Architecture%0A%0A%20%20%20%20%7C%20Layer%20%7C%20Technology%20%7C%20Purpose%20%7C%0A%20%20%20%20%7C-------%7C-----------%7C---------%7C%0A%20%20%20%20%7C%20Structural%20Model%20%7C%20SysMLv2%20RDF%2FTurtle%20(aliased%20to%20openCAESAR)%20%7C%20Requirements%2C%20design%20elements%2C%20satisfy%20links%20%7C%0A%20%20%20%20%7C%20Model%20Changes%20%7C%20SPARQL%20UPDATE%20%7C%20Modify%20parameters%2C%20trigger%20hash%20invalidation%20%7C%0A%20%20%20%20%7C%20Evidence%20Layer%20%7C%20PROV-O%20%2B%20EARL%20%2B%20OntoGSN%20%2B%20thin%20%60rtm%3A%60%20glue%20%7C%20Hash-bound%20evidence%20%2B%20GSN-structured%20attestation%20%7C%0A%20%20%20%20%7C%20Process%20Model%20%7C%20P-PLAN%20%7C%20Declarative%20pipeline%3B%20one%20%60p-plan%3AStep%60%20per%20stage%20%7C%0A%20%20%20%20%7C%20Closure%20Rules%20%7C%20SHACL%20%2B%20runtime%20re-verification%20%7C%2010%20well-formedness%20invariants%20enforced%20at%20Stage%206.5%20%7C%0A%20%20%20%20%7C%20Audit%20%7C%20Custom%20%60traceability.audit%60%20%7C%20Forward%20%2F%20backward%20%2F%20bidirectional%20with%20independence%20%7C%0A%20%20%20%20%7C%20Storage%20%7C%20rdflib%20%60Dataset%60%20(named-graph%20quadstore)%20%7C%20Eight%20named%20graphs%3B%20Flexo%2FFuseki-ready%20layout%20%7C%0A%20%20%20%20%7C%20Symbolic%20Analysis%20%7C%20SymPy%20ProofScripts%20%7C%20Formal%20proofs%20with%20re-verifiable%20lemma%20chains%20%7C%0A%20%20%20%20%7C%20Numerical%20Simulation%20%7C%20scipy%20solve_ivp%20%7C%20Time-domain%20ODE%20integration%20%7C%0A%20%20%20%20%7C%20Compute%20Provenance%20%7C%20Local%20%2B%20Docker%20backends%20%7C%20%60ExecutionMetadata%60%20%E2%86%92%20PROV%20triples%20per%20activity%20%7C%0A%20%20%20%20%7C%20Version%20Control%20%7C%20Git%20%7C%20Source%20of%20truth%20for%20all%20artifacts%20%7C%0A%20%20%20%20%22%22%22)%0A%20%20%20%20return%0A%0A%0A%40app.cell(hide_code%3DTrue)%0Adef%20_()%3A%0A%20%20%20%20import%20marimo%20as%20mo%0A%0A%20%20%20%20return%20(mo%2C)%0A%0A%0Aif%20__name__%20%3D%3D%20%22__main__%22%3A%0A%20%20%20%20app.run()%0A
c629c5fd7e512c6195b3881390701727