Repository navigation
[LEAN-6] Review pairings whose witnesses already specialize or refine #104
Description
Scope ID: LEAN-6. Size: Minor. Scoped on 2026-10-08 in SCOPE-2026-10-08.md; acceptance remains open.
Owner: formalism relations.
Dependencies: Independent
Work
Seven pairing witnesses are named specializes/refines/extends/bounds (e.g. fep089_…_specializes_fep006, fep092_…_specializes_fep032). Re-tag genuine instantiations as formal; keep pairings whose rationale says conventions are not identified.
Acceptance
At least 22 formal edges, each with a review note naming the consumed endpoint theorem.
Failure controls and claim boundary
A pairing is not an implication; re-tag only on review.
Canonical references
Closure requires actual exact-source commands, results and retained receipts, with independent review where specified. Remove its open TODO row only after acceptance; retain delivery facts in changelog/history. Size describes implementation scope, not a semantic-version promise.
Activity
docs: record pairing rationale tightening as proposed, not applied (#104
docxology commentedon Oct 9, 2026
Status update (2026-10-09). Review delivered in #159 (via #164). None of the seven witnesses qualifies for re-tagging: each conjoins two independently proved endpoint theorems, and neither is derived from the other. The review table is in
docs/relations-endpoint-adjudication.md. Five rationales overstate the link, and the tightened wording is recorded there as proposed. Released relation rows are digest-sealed (tests/test_formalism_catalogue_155.py), so applying it needs a reviewed seal delta. Remaining for closure: decide on the five proposed rationale rewrites and record them as reviewed edge deltas.docxology commentedon Oct 11, 2026
The relations file has 24
formaledges, which meets the count. All seven specializes/refines pairings were kept, perdocs/relations-endpoint-adjudication.md. Still open: only 5 of the 24 rationales name their consumed endpoint theorem, and the five proposed rewrites live only in the adjudication doc. Applying them is a reviewed seal delta. TheTODO.mdrow is narrowed in #171 to the remaining clause.