What the Lean Proof of ADIC Means for Responsibility Engineering

Recently, the core lemma of ADIC (Advanced Data Integrity by Ledger of Computation) was formally verified using Lean 4, and its proof script (ADIC_RSound.lean) has been publicly released.

In the context of software engineering and mathematics, formal proofs using theorem provers such as Lean are positioned as a powerful method for mechanically confirming the properties of theorems and verifiers. However, within the framework of "Responsibility Engineering" advocated by GhostDrift Research, the role of this proof occupies a different position from that of conventional formal proofs.

This article clarifies what the release of this Lean proof signifies within the ADIC architecture. By explicitly outlining four critical differences from general formal verification, we externally fix the structural reasons why we required formal proof.

1. Purpose: Pursuit of Truth vs. Fixing Responsibility Boundaries

The primary purpose of general formal proof is to mechanically verify properties regarding correctness for target theorems and algorithms under a given formal system.

In contrast, the purpose of formal proof in ADIC is to mathematically fix the boundary between "conditions to answer" and "conditions to remain silent or reject" in advance. The "responsibility boundary" here refers to a boundary—predetermined under given witnesses, specification constraints, and verification conditions—that defines the range where the system may accept an output versus where it must reject or abstain.

What ADIC addresses is the Algorithmic Legitimacy Shift (ALS). This refers to the phase where legitimacy, traditionally belonging to human judgment, shifts to the algorithmic side under certain conditions. In the irreversible regime where $B < J$ holds (with $B$ representing the observation cost and $J$ the threshold of legitimacy shift), this acceptance boundary must not rely on post-hoc interpretation.

The proof of ADIC does not prove that the program "outputs the correct answer." Rather, it serves as evidence to logically fix the "boundary of responsibility," ensuring that computations are reliably rejected or invalidated outside the pre-defined boundary (minimax structure). The objective here is to re-express the responsibility judgments—often questioned in the contexts of AI governance and accountability—not as post-hoc interpretations, but as predetermined mathematical conditions.

2. Structure: Closed Script vs. Three-Tier Architecture

In general formal proof projects, the proof script passing the kernel (i.e., achieving zero errors) often signifies the final goal of the project. The world is complete within the binary relationship between the theory and the proof code.

However, in ADIC, the proof script is merely an "intermediate layer." ADIC operates on a three-tier architecture: Theory $\rightarrow$ Formal Proof $\rightarrow$ Implementation. The newly released ADIC_RSound.lean proof inherits the Verifier Core defined in the theoretical paper and seamlessly connects it to the audit artifacts and append-only ledger in the implemented system.

In this sense, the proof is not an endpoint, but is positioned as a verification foundation (Proof as Infrastructure) supporting the operation of real-data systems.

3. Verification Target: Correctness of Internal Operations vs. Validity of External Evidence (Witness)

In standard formal proofs of programs, the target of the proof is whether the program itself can correctly execute complex internal computations (e.g., non-linear functional operations).

Conversely, as observing ADIC_RSound.lean makes clear, the verifier does not perform complex operations itself. In verifying operations like multiplication (WMul) and inversion (WInv), ADIC only determines whether the externally provided "evidence" (Witness) satisfies predetermined conditions (such as CheckMul and CheckInv).

This represents the core of Responsibility Engineering: clearly separating the executing entity (Prover) and the verifying entity (Verifier). We do not place the computational process directly constructing the correct answer at the center of the proof target; instead, we adopt a structure that re-verifies whether the presented witness satisfies fixed conditions. By utilizing this Witness-based structure, the room for reliance on post-hoc interpretation is significantly suppressed.

4. Extension: Static Truth vs. Social Implementation via Dynamic Ledger

General formal proofs remain at the confirmation of static mathematical truths, such as ensuring "this theorem is always correct."

However, in ADIC, formal proof does not remain closed within the theory but is connected to an auditable operational structure. ADIC adopts a Ledger / Witness / Verifier configuration based on interval arithmetic and finite closure, predicated from the outset on being verifiable in Lean (Lean-ready).

What Lean demonstrates is soundness: when the Verifier accepts the Witness conditions, the corresponding interval guarantees inherently hold. Based on this soundness, the relationship among the Ledger, Witness, and Verifier becomes operational as a verification path fixed in advance, rather than explained post-hoc.

Upon this verification infrastructure, at least for accepted outputs, it becomes possible to trace the precise evidence and conditions that formed the basis of the validity judgment.

Conclusion

The formal proof using Lean in ADIC is not primarily aimed at the general confirmation of mathematical truth or software quality assurance itself. Rather, it is positioned as an infrastructure to pre-fix the responsibility boundaries—determining what should be accepted, rejected, or abstained from—under given witnesses, specifications, and verification conditions.

In this sense, formal proof in ADIC serves not as an endpoint that closes the theory, but as an implementation infrastructure supporting auditability and accountability.