Why Responsibility Information Is Heavy: A Lean Formalization of the Distinctions AI Audit Logs Lose
- kanna qed
- 6月15日
- 読了時間: 7分
Introduction
AI audit logs usually record what happened.
For example:
```text
2026–06–15 10:00
AI system approved request X
score = 0.87
label = approved
```
This is useful.
But when we need to inspect responsibility later, it may not be enough.
The same `approved` result can mean very different things:
```text
The request was approved after all required conditions were verified.
```
or:
```text
The request was approved while some required conditions remained unverified.
```
In this article, I explain the idea behind the Lean repository:
```text
```
The core claim is:
> Responsibility information is not merely history.
> It carries distinctions that must be preserved for later audit, inspection, and verification.
> In that finite-capacity sense, responsibility information is “heavy.”
Here, “heavy” does not mean emotionally or morally heavy.
It means that responsibility information contains more distinguishable states that must not be collapsed.
This is not Shannon information theory.
It is about finite capacity: counting distinguishable responsibility-information states using `Fintype.card`.
— -
What Ordinary Logs Lose
Consider two cases.
Case A: Approved after full verification
```text
Human -> AI -> Approve
Condition A: verified
Condition B: verified
Condition C: verified
Unverified conditions: none
```
Case B: Approved with unverified conditions
```text
Human -> AI -> Approve
Condition A: verified
Condition B: unverified
Condition C: unverified
Unverified conditions: exist
```
From the perspective of a simple operational log, both may look like:
```text
AI approved
```
But as responsibility states, they are different.
The later audit question is not only:
```text
Was it approved?
```
The real questions are:
```text
What evidence was used?
Which conditions were verified?
What remained unverified?
Which version of the data was used?
Who was involved at which stage?
Was there a verifiable certificate?
```
If those distinctions disappear from the log, the responsibility state cannot be inspected later.
— -
Responsibility Information as “History + Fiber”
In the Lean file, responsibility information is modeled as:
```lean
abbrev ResponsibilityInfo
(History : Type u)
(EvidenceFor : History -> Type v) : Type (max u v) :=
Sigma EvidenceFor
```
This means:
```text
a history h
+
responsibility-relevant information over that history h
```
The second component, `EvidenceFor h`, may contain:
```text
evidence
provenance
verification status
unverified conditions
constraints
boundary information
audit metadata
ADIC certificates
```
The important point is that `EvidenceFor` is dependent:
```lean
EvidenceFor : History -> Type
```
So responsibility information is not just:
```lean
History × Evidence
```
It is:
```lean
Sigma EvidenceFor
```
Different histories may have different meaningful evidence, provenance, constraint, or certificate spaces.
This is why the dependent-sum structure matters.
— -
Projection to History Exists, but Reconstruction Does Not
From responsibility information, we can always project back to history:
```lean
def historyProjection
{History : Type u}
{EvidenceFor : History -> Type v} :
ResponsibilityInfo History EvidenceFor -> History :=
Sigma.fst
```
So there is a map:
```text
ResponsibilityInfo -> History
```
But the reverse direction does not generally exist.
If the same history supports multiple responsibility-relevant evidence states, then history alone cannot reconstruct the original responsibility information.
In Lean:
```lean
theorem history_projection_not_injective
(History : Type u)
(EvidenceFor : History -> Type v)
(h_two :
∃ h, ∃ e1 e2 : EvidenceFor h, e1 ≠ e2) :
¬ Function.Injective
(historyProjection :
ResponsibilityInfo History EvidenceFor -> History)
```
Informally:
> If there are two different evidence states over the same history,
> then the projection from responsibility information to history is not injective.
> Therefore, history alone does not determine responsibility information.
This is a basic but important point for audit-log design.
Once responsibility information has been collapsed into history-only logs, the original responsibility state may be unrecoverable.
— -
History-Only Logs Lose Responsibility Fibers
Many logs effectively observe responsibility information through history:
```text
ResponsibilityInfo -> History -> Log
```
That is, they first forget the responsibility fiber and then produce a log entry.
Such a log cannot distinguish different responsibility states over the same history.
The Lean file defines fiber-injectivity as:
```lean
def FiberInjective
{History : Type u}
{Q : History -> Type v}
{Log : Type w}
(obs : Sigma Q -> Log) : Prop :=
forall {h : History} {q1 q2 : Q h},
obs ⟨h, q1⟩ = obs ⟨h, q2⟩ ->
q1 = q2
```
An observation is fiber-injective when it can distinguish all responsibility states inside each history fiber.
A history-only log is not fiber-injective when a nontrivial responsibility fiber exists:
```lean
theorem history_factored_log_not_fiber_injective
{History : Type u}
{Q : History -> Type v}
{Log : Type w}
(alpha : History -> Log)
(h_two : exists h : History, exists q1 q2 : Q h, q1 ≠ q2) :
Not (FiberInjective (fun r : Sigma Q => alpha r.1))
```
In plain terms:
> Any log that factors only through history loses distinctions inside nontrivial responsibility fibers.
This is the formal reason why ordinary audit logs cannot replace responsibility information.
— -
Responsibility Information Has Larger Capacity Than History
For finite types, the capacity of responsibility information is counted as:
```lean
theorem responsibility_info_card
(History : Type u)
(EvidenceFor : History -> Type v)
[Fintype History]
[∀ h, Fintype (EvidenceFor h)] :
Fintype.card (ResponsibilityInfo History EvidenceFor)
=
∑ h : History, Fintype.card (EvidenceFor h)
```
That is:
```text
capacity of responsibility information
=
sum of responsibility-fiber capacities over all histories
```
If every history has at least one evidence state, and at least one history has more than one evidence state, then:
```lean
theorem responsibility_info_strictly_larger_than_history
```
proves:
```text
capacity of history < capacity of responsibility information
```
This is the minimal mathematical meaning of the phrase:
> Responsibility information is heavier than history.
— -
Relation to PROV
Information science already has the concept of provenance.
In W3C PROV, provenance describes how information is generated, transformed, or attributed through entities, activities, and agents.
In this formalization, PROV-style qualified provenance is treated as part of the responsibility fiber.
Intuitively:
```text
unqualified provenance relation
= history
qualified provenance node
= responsibility-relevant fiber over that history
```
For example, a simple relation such as:
```text
wasAttributedTo(entity, agent)
```
may be refined by:
```text
role
attributes
relation id
validity constraints
```
Those qualified elements may matter when we later inspect the responsibility state.
The repository models PROV-style qualified influence families such as:
```text
generation
usage
communication
start
end
invalidation
derivation
attribution
association
delegation
revision
quotation
primary source
```
In Lean, `end` is represented as `qualifiedEnd` to avoid keyword ambiguity.
This is not a full OWL implementation of W3C PROV-O.
It is a finite-capacity model of PROV-style qualified structures.
— -
ADIC Is a Certificate Fiber, Not a Label
ADIC is not a mechanism for attaching an `OK` or `NG` label to a log.
From the perspective of responsibility information, ADIC is a certificate fiber.
For a responsibility record, the ADIC layer asks:
```text
Does this record satisfy the committed boundary?
Was the evidence verified?
Were the constraints satisfied?
Can the verification result be checked later?
```
If there is no valid certificate, the record is not ADIC-verifiable.
If valid certificates exist, those certificates themselves become part of the responsibility information.
In that sense, ADIC is not a replacement for ordinary audit logs or threshold checks.
It is a certificate layer that makes responsibility information verifiable later.
— -
The Heavier the Responsibility, the More Distinctions Must Be Preserved
The claim is not only that responsibility information is heavier than history.
The stronger point is:
> The heavier the responsibility, the more distinctions must be preserved.
In the Lean file, this is modeled by required responsibility capacity at each responsibility weight:
```lean
abbrev RequiredResponsibilityInfo
(History : Type u)
(requiredCapacity : Weight -> History -> Nat)
(weight : Weight) : Type u :=
Sigma fun h : History => Fin (requiredCapacity weight h)
```
Here,
```lean
requiredCapacity weight h
```
is the number of evidence distinctions required for history `h` at a given responsibility weight.
The capacity of required responsibility information is:
```text
Σ h, requiredCapacity weight h
```
If increasing responsibility weight never decreases the required capacity for any history, then the required responsibility information capacity does not decrease.
If it strictly increases for at least one history while never decreasing elsewhere, then the total required responsibility information capacity strictly increases.
So the formal statement is:
> If higher responsibility weight requires more distinctions to be preserved,
> then higher responsibility weight requires larger responsibility-information capacity.
This matters in domains such as:
```text
human safety
finance
medical systems
logistics
infrastructure
public-sector decision-making
```
In such settings, a log entry like:
```text
approved
```
or:
```text
score = 0.87
```
is not enough.
The system must preserve:
```text
what evidence was used
which conditions were verified
what remained unverified
which boundaries were not crossed
which certificates existed
who was involved at which stage
```
— -
Verification Load, Not Physical Energy
When this article says responsibility information is “heavy,” it is not talking about physical energy.
The Lean file contains names such as `VerificationEnergy`, but for external explanation, `VerificationLoad` is clearer.
The intended meaning is operational burden:
```text
audit
storage
inspection
validation
re-checking
```
If responsibility-information capacity increases, the burden of preserving and verifying it also increases under any monotone load model.
That is the sense in which responsibility information becomes heavier.
— -
Terminology
The terminology used in this article corresponds to the following concepts.
| Term | Role in this article |
| — -| — -|
| Provenance | How information was generated, transformed, or attributed |
| Traceability | The ability to trace back from an action or result to its sources and actors |
| Audit Trail | A record of who did what and when |
| Metadata | Metadata becomes responsibility information only when needed to inspect responsibility state |
| Auditability | The ability to inspect a decision or process later |
| Verifiability | The ability to show correctness against rules, certificates, or constraints |
| State Transition | AI decisions are treated as state transitions, not merely outputs |
| Accountability-Relevant Information | Information that must not be lost if responsibility state must be inspected later |
| Accountability State | The state of who acted, based on what evidence, under which verified and unverified conditions |
| Information Loss | Collapse of responsibility states that should have remained distinguishable |
— -
Summary
Ordinary logs record what happened.
But responsibility inspection requires more than that.
It requires preserving:
```text
what evidence was used
which constraints were satisfied
what remained unverified
which certificates existed
which responsibility states had to remain distinguishable
```
Responsibility information is heavier than history.
This heaviness is not rhetorical or moralistic.
It is the finite capacity of responsibility-relevant fibers over history: the number of distinctions that must be preserved for later audit, inspection, and verification.
And when responsibility becomes heavier, the number of distinctions that must be preserved also increases.
Responsibility OS and ADIC are needed not because we expect AI systems to be ethical by themselves.
They are needed because history-only logs can lose the distinctions required to verify responsibility later.
コメント