Outcome Log Accountability Completion

Abstract

Outcome-only logs omit accountability, whose canonical completion is least.

Theorem 1.1 (Outcome-only logs cannot recover full accountability).

$$\begin{array}{c}\forall Z,Decision,Rule,Actor,Provenance:\mathrm{Type},\\ D:Z\to Decision,R:Z\to Rule,\\ A:Z\to Actor,P:Z\to Provenance,\\ z,zp:Z,\\ D\left(z\right)=D\left(zp\right)\wedge (A\left(z\right)\ne A\left(zp\right)\vee R\left(z\right)\ne R\left(zp\right))\Rightarrow \\ (\forall Log:\mathrm{Type},L:Z\to Log,\\ \mathrm{Refines}\left(L,D\right)\Rightarrow \neg \mathrm{Refines}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(D,R\right),A\right),P\right),L\right))\wedge \\ \forall Log:\mathrm{Type},L:Z\to Log,\\ \mathrm{Refines}\left(L,\mathrm{conceptJoin}\left(L,\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(D,R\right),A\right),P\right)\right)\right)\wedge \\ \mathrm{Refines}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(D,R\right),A\right),P\right),\mathrm{conceptJoin}\left(L,\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(D,R\right),A\right),P\right)\right)\right)\wedge \\ \forall Candidate:\mathrm{Type},K:Z\to Candidate,\\ (\mathrm{Refines}\left(L,K\right)\wedge \mathrm{Refines}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(D,R\right),A\right),P\right),K\right))\Rightarrow \mathrm{Refines}\left(\mathrm{conceptJoin}\left(L,\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(\mathrm{conceptJoin}\left(D,R\right),A\right),P\right)\right),K\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Audits/OutcomeLogAccountabilityCompletion.outcome_log_obstruction_and_accountability_completion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Decision, rule, actor, and provenance are independent readouts on the same state carrier. Their nested canonical join is the full accountability readout.

A log that factors through the decision identifies the displayed witness states. Their different actor or rule coordinate makes the full accountability readout vary on that log fiber, so no recovery factor can exist.

Joining the log with the accountability readout retains each component. Pairing any two supplied factors proves that this completion is below every common refinement.

References

• Truth anchor: D5/S3/ConceptDynamics/Audits/OutcomeLogAccountabilityCompletion.outcome_log_obstruction_and_accountability_completion
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/ConceptDynamics/NormativeStructure/HistorySensitiveOutcomeReductionObstruction