# Proof certificates and DAGs

[All sections](../README.md)

## Modules

| Module | Verified result |
|---|---|
| [ProofGraphDAG](ProofGraphDAG.en.md) | A computable checker for certificate trees and conditional soundness of accepted conclusions. |
| [ProofGraphAcyclic](ProofGraphAcyclic.en.md) | References to strictly smaller indices exclude cycles; conditional soundness of sequential DAG evaluation. |

## Scope

Soundness retains the assumptions on rule validity and certificate interpretation. This is not a blockchain consensus or distributed execution proof.

[Contributing](../CONTRIBUTING.en.md) · [Validation](../VERIFICATION.en.md)

- [Rational polynomial certificates](AlgebraicCertificateKernel.en.md)

- [Normalization completeness and rejection soundness](AlgebraicCertificateCompleteness.en.md)

- [Canonical ASCII JSON syntax](AlgebraicCertificateSyntax.en.md)

- [Typed ALCC schema decoding](AlgebraicCertificateSchema.en.md)

- [Byte-to-task composition](AlgebraicCertificateUnbound.en.md)

- [SHA-256 functional refinement](AlgebraicCertificateSHA256.en.md)

- [Binding to the supplied passport](AlgebraicCertificateBound.en.md)

- [Canonical bytes to certificate verdict](AlgebraicCertificateVerify.en.md)

- [Coefficient-caching normalization pilot](AlgebraicCertificateNormalizeCached.en.md)