Cortex Proof Status

This page tracks human claims, not raw theorem counts. A single claim may be backed by several Lean declarations, and a proved Lean theorem is not the same thing as executable Haskell correspondence. The matrix keeps those layers separate.

Summary

These numbers are intentionally conservative. “Haskell-linked” means the implementation has a specific check, report, witness constructor, or regression surface connected to the claim. It does not mean the compiler is extracted from Lean or that every witness field is produced by a shared oracle.

Status Key

Compiler Admission Gates

Compiler hygiene gates are tracked outside the proof-claim denominator. For example, duplicate and prefix-conflicting CorePure record paths are rejected before evaluation and covered by Haskell compiler/runtime tests, but they are parser/elaborator admission checks rather than admitted-middle Lean safety claims. If the parser or compiler is later mechanized, those gates can become proof rows.

Matrix

Wire Admission Notes

• The current Wire admission correspondence target is deliberately staged: Haskell emits schema-versioned JSON metadata, the executable Haskell validator decides wireAdmissionArtifactValidatorReady, Lean mirrors that predicate as AdmissionArtifact.ValidatorReady, and AdmissionArtifact.validatorReady_sound packages the resulting primitive, generated-form, select, and phantom-adapter obligations as AdmissionArtifact.Sound. That is the established cutline for this PR.
• Lean now owns an executable primitive-stack replay checker: AdmissionArtifact.primitiveTraceStackValidCheck_sound proves that a successful check implies the relational PrimitiveTraceStackValid obligation. AdmissionArtifact.validatorReadyCheck_sound now lifts the same Lean-owned executable strategy to the full ValidatorReady contract: schema version, summary-key uniqueness, summary-row validity, summary domain closure, summary identities matching primitive rows, summary frontiers backed by primitive rows, exact summary residual-frontier matching, raw connections matching primitive rows, component-domain closure, component-row uniqueness, generated-form reference anchoring, component frontier backing, generated-child frontier exactness, primitive stack replay, primitive overlay ledger prefix availability, primitive connect frontier backing, primitive connect frontier prefix availability, select bridge frontier backing, select bridge entry consumption, select arm body-boundary matching, select body-node freshness, select body-node disjointness, phantom bridge frontier backing, phantom bridge frontier exactness, phantom bulk replay, primitive row validity, local generated-form validity, local phantom-adapter validity, and local select-row validity. AdmissionArtifact.validatorReadyCheck_soundness then composes that result with AdmissionArtifact.validatorReady_sound to produce AdmissionArtifact.Sound. Haskell integration still needs to run this checker on decoded artifacts; the Lean checker is now the intended artifact-validation authority.
• Primitive artifact replay now has an explicit reconstruction target: AdmissionArtifact.PrimitiveGraphReconstruction. From AdmissionArtifact.Sound, AdmissionArtifact.Sound.toPrimitiveGraphReconstruction recovers the final primitive replay frame, proves it matches the top-level summary, proves source-visible primitive rows are duplicate-free, classifies every primitive frontier key as exposed, consumed, or select-internal, and keeps raw-connection projection tied to replayed primitive contractions. This is intentionally not yet GraphElaboration.CertifiedGraph: accepted-node declarations and binding expansion are still separate correspondence evidence.
• Generated-form artifacts now have the same kind of artifact-boundary reconstruction: AdmissionArtifact.GeneratedReconstruction. AdmissionArtifact.Sound.toGeneratedReconstruction proves that persisted make/makeEach rows recover accepted source MakeItems, unique source child provenance for each surviving generated node, primitive-backed child frontiers, frontier-key accounting through primitive replay, canonical value-free make payloads, and decoded static payload projection. This is intentionally not yet KindInstantiatedFrontiers or MakeWitness; accepted-kind substitution evidence is still the next boundary.
• Phantom-adapter artifacts now also reconstruct at the artifact boundary: AdmissionArtifact.PhantomReconstruction. AdmissionArtifact.Sound.toPhantomReconstruction proves that every persisted * row has a primitive-backed generated adapter node, a source-linear open phantom-node object, frontier-key accounting through primitive replay, replayed left/right bulk rows, direction-specific multi/singular endpoint coverage, and record or bounded-indexed product-shape evidence. This is intentionally not yet PhantomAdapterWitness: the serialized row does not contain the left/right operand objects or certified BulkContract traces.
• Select-admission artifacts now reconstruct at the artifact boundary: AdmissionArtifact.SelectReconstruction. AdmissionArtifact.Sound.toSelectReconstruction proves that every persisted select(...) row has projected latent-admission key coverage, source arm provenance, label-first or unique-contract-fallback resolution evidence, latent body freshness and pairwise body disjointness, condition-bridge/body-boundary shape evidence, and selected-variant bridge entry consumption. This is intentionally not selected-branch durable recovery: replaying the chosen latent body remains a separate recovery witness.
• The remaining end-to-end compiler theorem is stronger than Sound: it must show that every accepted Wire program causes the Haskell compiler to emit an artifact satisfying the validator, and that decoded rows can be replayed into the concrete Lean witnesses consumed by graph admission, generated-form admission, select recovery, and phantom-adapter insertion. Those completeness and executable-decoder correspondence proofs are intentionally outside this PR.
• Haskell admission artifacts now validate exact select bridge entry consumption and phantom-adapter bulk replay; the Lean mirror exposes these as AdmissionArtifact.SelectBridgeEntriesConsumed, AdmissionArtifact.PhantomBridgeBulkConnectionsReplayed, and matching ValidatorReady projection theorems. Primitive overlay/connect rows also expose prefix availability and compatible-pair consumption, so artifact replay order and boundary-pair use are available without unfolding the stack validator.
• Generated-family artifact handoff is now source-row exact: Lean recovers a unique source generated-child row for every surviving child row, preserves the source payload, exposes binding-owned generated node names, and surfaces per-child frontier validity and uniqueness through AdmissionArtifact.ValidatorReady accessors.
• Phantom-adapter artifact handoff now exposes row and domain facts directly: Lean names the product-shape, multi-side, singular, and left/right bulk-row obligations that Haskell validates, including stronger boundary closure over optional exclusive-group owners, record boundary labels, record aggregate-contract rows, indexed element-contract rows, nested-indexed element rejection, and singular endpoint equality with the serialized aggregate product contract. Admission artifact schema version 3 carries the record aggregate contract explicitly so the Haskell row can be checked against the Lean product-shape contract instead of being inferred from record fields.
• Primitive replay has per-branch exactness theorems for empty, node, binding-reference, overlay, and connect rows, and select admission exposes label-resolution uniqueness, contract-fallback uniqueness, and identity/non-identity body-shape projections from the emitted artifact rows.
• The Haskell compiler now gates metadata emission through wireAdmissionArtifactValidatorReady, so compiled circuits cannot publish a schema-versioned admission artifact that fails the same executable predicate mirrored by Lean’s AdmissionArtifact.ValidatorReady target.
• SelectedBranchRecoveryRecord.PhantomAdapterEmbedding is the recovery-side hook for the case where a selected branch contains a finite-product * adapter. The embedding theorem proves the persisted adapter node is replayed by the selected branch and pruned from every unselected branch.

How To Read The Counts

The numerator is the number of dashboard claims at that status. The denominator is the current dashboard goal set: the 28 claims above. Adding a new semantic claim should increase the denominator instead of hiding work inside an existing row.

The strictest question is not “is there a Lean theorem?” but:

semantic claim
  -> Lean statement
  -> Lean proof
  -> Haskell witness or oracle
  -> runtime path consumes that witness

Most open work is in the last two steps. The Lean side is now substantially ahead of the executable correspondence surface.

Related

• ../ADRs/0038-wire-proof-track-theorem-ledger.md — detailed theorem ledger.
• ../Architecture/03-formalism-stack.md — formalism stack.
• ../Architecture/05-wire-language.md — Wire architecture.
• development.md — local Lean and docs commands.