← Four-qubit Bacon-Shor subsystem 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
primarysubsystem-gaugee2eb2c5a42f4116b…
  • small-exact-distance-enumeration
  • structural-validity