← Surface code

Entry facet

Formal IR & certificates

Canonical finite-object identities and the exact Lean Complete v1 certificate classes checked for each shipped instance.

Each shipped finite instance has one canonical Formal IR semantic identity and a Lean-checked structural certificate. Eligible small exact-distance certificates are additive; claims outside Lean Complete v1 keep their existing evidence origin.

InstanceNative branchSemantic hashCertificates
L3css-chain8442e560b9de5fb4…
  • small-exact-distance-enumeration
  • structural-validity
L4css-chain14dbc9bd9de60b83…
  • small-exact-distance-enumeration
  • structural-validity
L5css-chaindf1d7dff6245677c…
  • structural-validity