Correction register
What We Got Wrong—and What Survives
Retraction is part of the research record. These entries preserve the original artifact, state the failure plainly, and identify the narrower result—if any—that remains usable. Current status is generated from one machine-readable ledger.
Compositional Accountability
The proposed packing-separator, administrative-cut, and complexity contributions reduce to temporal-separator, Minimum Label Cut, and Test Cover prior art; the lane is engineering-only.
Current scope: The source-only finite profile computes an exact model-relative query-answerability margin and replayable erasure certificate; it does not assess occurrence truth, non-equivocation, authority, remedy, or external validity.
BABEL v2
Earlier internal and annotation-derived results do not establish execution-failure prediction.
Current scope: No independent workflow evidence currently validates structural signals as predictors of execution failure.
BABEL v1
The frozen benchmark remains a reproducible historical artifact, but its internal structural labels do not establish execution-failure prediction.
Current scope: The frozen benchmark and its disclosed evaluations remain reproducible within their stated protocol; broader execution-prediction interpretations are retired.
The Disclosure Deficit
Consolidates only surviving results from the withdrawn fee-family papers; the spanning-tree basis count it replaces was wrong.
Current scope: The disclosure deficit is a difference of two signed-incidence ranks, equal to the hidden-field count minus the number of components those fields touch, and the rank identity is field-independent by total unimodularity.
The Coherence Fee gateway essay
The schema fee did not predict execution failure; the old gateway is retained for history only.
Current scope: No current headline claim; replaced as the program front door.
The Coherence Fee Paper I
Corollary 3.2 is false; surviving component-count results move only through the consolidated report.
Current scope: Historical source only.
The Witness Gram Paper III
The published basis-count corollary is false; the erratum and corrected repair result control.
Current scope: Historical source only; valid rank identities may be reused after line-by-line audit.
Witness Geometry Beyond Scalar Fee
The operational-sparsity claim was withdrawn; exact repair-basis results require the correction note.
Current scope: Historical source only.
Coherence Types
The type-soundness theorem is false under the stated rules; the static fragment does not rescue the theorem.
Current scope: Historical source only.
The Linear Communication Bottleneck Conjecture
The spectral-gap trichotomy is withdrawn; only the Haar marginal and adjacent-edge pairwise-independence lemmas survive.
Current scope: Surviving scoped result: random-encoder Procrustes edges have exact Haar marginals and exact adjacent-edge pairwise independence.
Column-Matroid Backbone
The former hierarchical-fee/lean evidence path did not exist. Adjacent checked rank identities are narrower than the whole paper; its corank identification is a written mathematical claim, not cleared here by those declarations.
Current scope: The scoped fee is a column-matroid corank under the paper's construction and hypotheses.
Signed-Incidence Structure
Lean support is the signed-incidence determinant/total-unimodularity step in the completed archived source. The named fee_field_independent declaration concludes True; the field-rank consequence is a written nonzero-minor argument, not that declaration.
Current scope: The completed archived Lean source proves signed_incidence_det_in_unit; field independence is the written consequence through nonzero minors.
A Witness Logic for Semantic Composition
Lean verifies the abstract numerical layer; the modeling identification remains review-dependent.
Current scope: Numerical uniqueness over the abstract DoctrineCarrier is machine-checked.
SCPI
conservativity_descent returns a conclusion already provided for arbitrary model classes by h_local; this does not establish general model-theoretic descent.
Beth.lean compiles but abstracts implicit and explicit definability to bare propositions; it is not evidence for semantic Beth definability, constructivity, or interpolation extraction.
The geometric and general Beth-for-sites arguments are prose-derived, nonconstructive, unmechanized, and under review.
Current scope: Finite Z/2 overlap examples, a concrete incompatible predicate pair, and set-valued gluing over a finite indexed cover are machine-checked; general conservativity and Beth are not.
Bridge
The frozen hidden-repair study is a candidate-generation baseline, not an independent Gate 2, Gate 3, or frontier-model canonization test.
Current scope: On the disclosed hidden-repair study, 14 of 15 classifications matched the predicted repair type exactly, one matched partially, and none missed.
Interpretability Frontier
Archived to enforce the no-fourth-family rule during the reset.
Current scope: In the paper's controlled cyclic-composition regime, edge-local interpretability features did not recover the global structural signal.
Interpolant Envelope
Beth for geometric sites is not treated as a constructive extractor; the public claim is restricted to the checked finite core.
Current scope: In the declared finite FRSL-1 semantics, full definitions, partial RELY and REFUSE regions, and same-reduct non-definability certificates can be independently checked.
No Free Precedent
The compounding observation is internal and captive; it is not foreign transfer, legal validity, or economic value.
Current scope: Case labels on a proper subset do not determine an unseen case absent an explicit hypothesis restriction; operative precedent requires reason, authority, scope, closure, epoch, and applicability.