Skip to content

docs: past-present-future doctrine (STATUS + PROOF-NEEDS rewrite + README banner + L3 diagram + .v signposts)#184

Merged
hyperpolymath merged 1 commit into
mainfrom
docs/past-present-future-doctrine
May 27, 2026
Merged

docs: past-present-future doctrine (STATUS + PROOF-NEEDS rewrite + README banner + L3 diagram + .v signposts)#184
hyperpolymath merged 1 commit into
mainfrom
docs/past-present-future-doctrine

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Single-PR landing of the orientation doctrine that prevents future sessions from "redoing the old stuff". Seven coordinated artefacts so the doctrine catches every reader at every entry point — human or machine.

Files

Type File Purpose
NEW STATUS.adoc Single-page past / present / future map at repo root. The doc that answers "where are we?" with a top-of-document disambiguation banner (ephapax ≠ AffineScript).
REWRITE PROOF-NEEDS.md Per-sublanguage proof debt audit, separated for ephapax-linear and ephapax-affine. Sections: done / todo / banned (6 anti-pattern categories) / counts. Replaces the prior version which still carried the pre-discovery legacy-preservation closure plan as viable.
PATCH README.adoc Foundational-redesign-in-progress banner; replaces pre-discovery "12 admits / 910 closed" Coq narrative with post-discovery per-layer picture; adds "Three superpowers" section with the NOT-a-tracing-GC-replacement caveat; adds "What this enables" (GDPR / verified resource management / policy enforcement); doc-map updated.
PATCH formal/PRESERVATION-DESIGN.md §6 One-sentence anchor + ASCII diagram + 3-point explanation of L3 architecture (one type former, two observation disciplines, one-way Linear→Affine via degrade).
BANNER formal/Semantics.v 🛑 ARCHAEOLOGY — do not extend
BANNER formal/Typing.v 🛑 ARCHAEOLOGY — Counterexample.v depends on falsity
BANNER formal/Semantics_L1.v ✅ ACTIVE — 9 admits are L2-integration debt
BANNER formal/TypingL1.v ✅ ACTIVE — judgment 100%, modality-indexed
BANNER formal/Modality.v ✅ ACTIVE — L2 (thin poset); L3 must not pattern-match
BANNER formal/Echo.v ✅ ACTIVE — ONE type former; do not split LinearEcho/AffineEcho
BANNER formal/Counterexample.v 📌 PINNED REGRESSION WITNESS — do not weaken

Disambiguation reinforced

STATUS.adoc opens with a CAUTION callout aimed at both human + machine readers: Ephapax ≠ AffineScript; ephapax-affine (the sublanguage inside this repo) ≠ AffineScript. The lexical overlap of "affine" is a coincidence of substructural-logic terminology, not a project relationship. PROOF-NEEDS.md leads with the same disambiguation. The README's existing IMPORTANT callout is strengthened with the cross-repo lesson-warning.

Safety envelope

  • No .v semantic changes.
  • No new Admitted or Axiom introduced.
  • No legacy code touched (Semantics.v, Typing.v) except top-of-file banner comments.
  • L1, L2, L3 calculi unchanged.
  • Counterexample.v unchanged.

Closes

This PR is the canonical post-discovery doctrine landing. It supersedes the in-flight #154 (filed 2026-05-26 with pre-consolidated framing). #154 will be closed in a follow-up after this lands; any unique linguistically-safe file-additions from #154 (EXPLAINME.adoc, EPHAPAX-VISION.adoc, spec/SPEC.md, site/index.md, ephapax-linear/README.md, TOPOLOGY.md) can be ported in a smaller follow-up with the current framing.

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

…EADME banner + PRESERVATION-DESIGN §6 diagram + .v file signposts

Single-commit landing of the orientation doctrine that prevents
future sessions from "redoing the old stuff". Seven coordinated
artefacts so the doctrine catches every reader at every entry point:

1. NEW `STATUS.adoc` at repo root — single-page past / present /
   future map with the disambiguation banner up front
   (ephapax ≠ AffineScript, ephapax-affine ≠ AffineScript).
   The doc that answers "where are we?" in one read.

2. `README.adoc` — adds a foundational-redesign-in-progress
   banner, replaces the pre-discovery "12 admits / 910 closed"
   Coq narrative with the post-discovery per-layer picture,
   adds a "Three superpowers" section (accountability of
   irreversible reclamation, selective reversibility via
   thin-poset, debugging/provenance via Linear Echoes) with
   the explicit "NOT a tracing-GC replacement" caveat, adds
   a "What this enables" section (GDPR-style certified
   erasure, verified resource management, machine-checkable
   policy enforcement), updates the documentation map to
   point at STATUS.adoc + PROOF-NEEDS.md + PRESERVATION-DESIGN.md
   as the canonical surfaces.

3. `PROOF-NEEDS.md` — complete rewrite. Per-sublanguage proof
   debt audit separated for ephapax-linear and ephapax-affine.
   Sections: what's done (Qed), what's todo (active work by
   layer), what's banned (explicit do-not-do anti-pattern
   detector — 6 categories including the AffineScript
   conflation trap), counts + file-by-file map. Replaces the
   prior PROOF-NEEDS.md which still carried the
   pre-discovery legacy-preservation closure plan as if
   viable.

4. `formal/PRESERVATION-DESIGN.md §6` — adds a one-sentence
   anchor ("L3 is the one place ephapax mechanises what
   happens to the information that an irreversible step
   erases") + an ASCII diagram showing the L3 architecture:
   one type former (the echo, a fiber), two L2-inherited
   observation disciplines (Linear ≤ Affine as a thin
   poset), one-way Linear ⟶ Affine degrade map (the
   no-section-collapse-to-residue proof). Plus a 3-point
   explanation precisely calling out what the diagram makes
   precise (Echo lives in L3; Linear/Affine don't live in
   L3; the arrow is one-way).

5. `.v` file banner comments — file-level signposts so
   anyone editing proof code is warned at the source:
     - formal/Semantics.v       — 🛑 ARCHAEOLOGY, do not extend
     - formal/Typing.v          — 🛑 ARCHAEOLOGY, Counterexample.v depends on falsity
     - formal/Semantics_L1.v    — ✅ ACTIVE, 9 admits are L2-integration debt
     - formal/TypingL1.v        — ✅ ACTIVE, judgment 100%, modality-indexed
     - formal/Modality.v        — ✅ ACTIVE, L2 (thin poset), L3 must not pattern-match
     - formal/Echo.v            — ✅ ACTIVE, ONE type former, do not split LinearEcho/AffineEcho
     - formal/Counterexample.v  — 📌 PINNED REGRESSION WITNESS, do not weaken

The architectural framing follows the owner directive of
2026-05-27 (CLAUDE.md "Owner directive" section) and the
canonical disambiguation doc at
`hyperpolymath/nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md`.

No `.v` semantic changes; pure docs + file-header banners.
Counterexample, L1, L2, L3 calculi all preserved. No new
`Admitted` or `Axiom` introduced.

Refs the 2026-05-26 counterexample landing
(`formal/Counterexample.v`, 5 Qed) and the L2-hybrid
landing (PRs #176 + #177).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit ed84e35 into main May 27, 2026
6 of 15 checks passed
@hyperpolymath hyperpolymath deleted the docs/past-present-future-doctrine branch May 27, 2026 15:10
hyperpolymath added a commit that referenced this pull request May 27, 2026
…notes (#185)

## Summary

Cherry-picked from the deleted orphan branch
\`lemma-b-phase2-middle-narrow\`, which carried 14 commits dated
2026-05-26 attacking \`formal/Semantics.v\` via the now-banned Lemma B
patterns (per CLAUDE.md owner directive 2026-05-27 DO-NOT #2).

**Only the audit/session-note documentation is cherry-picked.** The
Semantics.v changes are deliberately left behind.

## What lands

- \`docs/reports/audit/audit-2026-05-26-lemma-b-option-2-obstacle.md\` —
the audit document that records *why* Lemma B Phase 2 Option 2 hit a
real obstacle. Useful historical record of the pathway to the
counterexample.
-
\`docs/reports/audit/audit-2026-05-26-standards-134-reconciliation.md\`
— the reconciliation against standards#134 ground truth.
- \`docs/sessions/SESSION-2026-05-26-lemma-b-pivot.adoc\` — the session
note on the pivot.

Each file gets a prepended archaeology banner explaining that it
predates the counterexample and should NOT be applied as instructions —
readers should consult \`STATUS.adoc\` +
\`formal/PRESERVATION-DESIGN.md\` + \`PROOF-NEEDS.md\` for the current
doctrine.

## Companion to #184

This PR pairs with #184 (just-merged past-present-future doctrine
landing). Together they complete the historical-record preservation
while ensuring the post-discovery framing is what future readers and
sessions land on.

## After merge

Orphan branch \`lemma-b-phase2-middle-narrow\` will be deleted.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 27, 2026
Follow-up to #184 + #185. Aligns 5 secondary entry surfaces (EXPLAINME,
TOPOLOGY, docs/vision, ephapax-linear/README,
.machine_readable/META.a2ml) with the post-counterexample doctrine.
ROADMAP.adoc + .gitignore + .gitattributes + wiki deferred (not blocking
proof work). See commit body for per-file detail.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 51 issues detected

Severity Count
🔴 Critical 9
🟠 High 9
🟡 Medium 33

⚠️ Action Required: Critical security issues found!

View findings
[
  {
    "reason": "Issue in abi-verify.yml",
    "type": "unknown",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "unknown",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "unknown",
    "file": "scorecard-enforcer.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant