allKnownEvidenceGapsClosed · PR #298noOpenObligations · PR #300allCriteriaAccepted · PR #300noUntriagedOQs · PR #309| Layer | Name | Status | Source |
|---|---|---|---|
| L0 | Residue marker | stable | PR #272 (kernel) |
| L1 | Point certificate | stable | PR #272 / #267 |
| L1.5 | Registry flag | stable | PR #293 / #295 |
| L2 | Family slot | stable | PR #295 (#294) |
| L3 | CI invariant | stable | PR #298 (#296) |
| L4 | Policy schema | stable | PR #300 (#297) |
| L4-run | Orchestrator V1 | experiment | Issue #301 |
| L5 | Project ratification | human | out of scope (manual) |
| Seed | Kind | Status | Priority |
|---|---|---|---|
| empty | |||
| OQ id | Status | Evidence | Pressure seed |
|---|---|---|---|
| empty | |||
| Entry | Kind | External | E2E | Counterex | Rounds |
|---|---|---|---|---|---|
| BridgeC1C2Redundancy | growthTrace | no | no | false | 3 |
| BridgeC6GlobalCoverageAlignment | objectTheorem | no | no | false | 2 |
| GraphConnectivity | genericKernel | yes | no | false | 1 |
| PathCert | genericKernel | yes | no | false | 2 |
| DiameterAtMostTwoCert | genericKernel | yes | no | true | 2 |
| E2E_CompleteDigraphCert | e2eDiscovery | yes | yes | true | 2 |
| E2E_ReachStepCert | e2eDiscovery | yes | yes | false | 2 |
| E2E_SelfLoopCert | e2eDiscovery | yes | yes | true | 2 |
| E2E_FSM_InitIsAcceptingCert | e2eDiscovery | yes | yes | true | 2 |
| E2E_FSM_ExplicitInputCert | e2eDiscovery | yes | yes | false | 2 |
| E2E_FSM_AcceptingStateExistsCert | e2eDiscovery | yes | yes | true | 2 |
| Slot | Classification | Obligations |
|---|---|---|
| CompleteDigraphSlot | sufficient_only | forwardAdequacy:closed counterexample:closed |
| ReachStepSlot | equivalent | forwardAdequacy:closed iffEvidence:closed |
| InitIsAcceptingSlot | sufficient_only | forwardAdequacy:closed counterexample:closed |
| ExplicitInputSlot | equivalent | forwardAdequacy:closed iffEvidence:closed |
| Theorem | File | Source |
|---|---|---|
| allKnownEvidenceGapsClosed | lean/crt/MSTAutoGrowDiscoveryRegistryMWE.lean | PR #298 (#296) |
| noOpenObligations | lean/algorithms/MSTAutoGrowCriterionPolicyMWE.lean | PR #300 (#297) |
| allCriteriaAccepted | lean/algorithms/MSTAutoGrowCriterionPolicyMWE.lean | PR #300 (#297) |