A total without a receipt

A policy resolver returns “enabled” but cannot say which source and rule caused it. Logs are incomplete, reordered, and tied to one execution. Attach a token to each input fact and carry symbolic reasons through evaluation.

A provenance semiring supplies zero and one, addition for alternative proofs, and multiplication for joint premises. Associativity and distributivity let query rewrites preserve annotations along with answers. Substituting different interpretations later can answer lineage, trust, or multiplicity questions.

Proof objects generalize the discipline: a decision carries a finite derivation whose steps a checker can validate. Explanation becomes a value at the semantic boundary rather than prose reverse-engineered from effects.

Where the model stops

Provenance explains derivation under the modeled rules; it does not prove the inputs were true. Symbolic expressions may grow, so representations need sharing and explicit bounds. Operational debugging still needs traces for latency and failures not present in the semantic proof.

Lessons

• Reasons can compose with answers.
• Addition represents alternatives; multiplication represents joint premises.
• A proof object is checkable semantic evidence.
• Provenance does not certify source truth.

Practice

1. Build the expression for an answer requiring X and either Y or Z.
2. Distinguish provenance from an execution log.
3. Transfer the model to authorization or configuration resolution.

Part VII asks whether raw numbers have discarded equally important context: units and frames.

References

1. “Todd Green, Gregory Karvounarakis, and Val Tannen, “Provenance Semirings”.” — the semiring model of database provenance.