← Bacon–Shor 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
rectangle_3x5subsystem-gaugeb0d377ae17fea267…
  • small-exact-distance-enumeration
  • structural-validity
square_2subsystem-gauged8e746166aa33cd2…
  • small-exact-distance-enumeration
  • structural-validity
square_3subsystem-gauge5c0662072db371fa…
  • small-exact-distance-enumeration
  • structural-validity