← Bivariate bicycle 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
grosscss-chain74f45e7bdf312215…
  • structural-validity
toric_L3css-chainb469c20c64c071b1…
  • small-exact-distance-enumeration
  • structural-validity