Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions docs/reports/audit/audit-2026-05-26-lemma-b-option-2-obstacle.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,24 @@
<!--
🛑 ARCHAEOLOGY DOCUMENT — preserved for the pathway-to-counterexample record.

This audit was written 2026-05-26 BEFORE the verified Coq counterexample
(formal/Counterexample.v, 5 Qed) showed that the preservation theorem
it attempts to close is provably false.

Its conclusions / closure plans / "just one more lemma" framings are
pre-discovery. DO NOT apply them to current proof work.

The post-discovery doctrine lives at:
- STATUS.adoc (past / present / future map)
- formal/PRESERVATION-DESIGN.md (four-layer architecture)
- PROOF-NEEDS.md (per-sublanguage proof debt)
- CLAUDE.md (owner directive 2026-05-27)

This file is preserved because the audit text DOCUMENTS the obstacle
that led to the counterexample discovery — useful historical record,
not instructions.
-->

<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->

# Audit Report: ephapax — 2026-05-26 — Lemma B Phase 2 Option 2 obstacle
Expand Down
Original file line number Diff line number Diff line change
@@ -1,3 +1,24 @@
<!--
🛑 ARCHAEOLOGY DOCUMENT — preserved for the pathway-to-counterexample record.

This audit was written 2026-05-26 BEFORE the verified Coq counterexample
(formal/Counterexample.v, 5 Qed) showed that the preservation theorem
it attempts to close is provably false.

Its conclusions / closure plans / "just one more lemma" framings are
pre-discovery. DO NOT apply them to current proof work.

The post-discovery doctrine lives at:
- STATUS.adoc (past / present / future map)
- formal/PRESERVATION-DESIGN.md (four-layer architecture)
- PROOF-NEEDS.md (per-sublanguage proof debt)
- CLAUDE.md (owner directive 2026-05-27)

This file is preserved because the audit text DOCUMENTS the obstacle
that led to the counterexample discovery — useful historical record,
not instructions.
-->

<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->

# Audit Report: ephapax — 2026-05-26 — standards#134 reconciliation
Expand Down
16 changes: 16 additions & 0 deletions docs/sessions/SESSION-2026-05-26-lemma-b-pivot.adoc
Original file line number Diff line number Diff line change
@@ -1,3 +1,19 @@
////
🛑 ARCHAEOLOGY DOCUMENT — preserved for the pathway-to-counterexample record.

This session note records the 2026-05-26 Lemma B pivot, BEFORE the
verified Coq counterexample (formal/Counterexample.v, 5 Qed) showed
that the preservation theorem it attempts to close is provably false.

Its conclusions / closure plans / "just one more lemma" framings are
pre-discovery. DO NOT apply them to current proof work.

Post-discovery doctrine: STATUS.adoc + formal/PRESERVATION-DESIGN.md
+ PROOF-NEEDS.md + CLAUDE.md (owner directive 2026-05-27).

This file is preserved for historical accuracy, not as instructions.
////

// SPDX-License-Identifier: PMPL-1.0-or-later
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
= Session: Lemma B Phase 2 — case-count truthing + Option 2 obstacle + Path 1 pivot (2026-05-26)
Expand Down
Loading