hyperpolymath · hyperpolymath · Jun 24, 2026 · Jun 24, 2026
@@ -7,8 +7,8 @@
 @state(version="2.0"):
 phase: "implementation"
 next_action: "Phase D slice 4 Phase 3b Stages 2-4 (#240/#241/#242): Stage 1 (both 1a + 1b) complete. Stages 2-4 sequenced per the owner-approved 4-stage plan: Stage 2 (#240) ELam annotation extension — independent of Stage 1, ships when prioritised; Stage 3 (#241) CPS + relaxed Phase 3b — blocked on Stage 2; Stage 4 (#242) compound non-linear + unconditional preservation_l2 — blocked on Stage 3. Stage 4's destination collapses Stage 1b's three preconditions (P1 = tfuneff_lambda_free, P2 = regions_introduced_by ⊆ R_in_v, P3 = expr_closed_below 0 v) once typing-derived closure invariants land. Anti-patterns to refuse (per CLAUDE.md owner directive): no `Admitted`; no touching `Semantics.v` / `Typing.v` / `Counterexample.v`; no closure of residual `Semantics_L1.v` admits — strictly NEW infrastructure orthogonal to legacy. Coqc 8.18.0 is the only authority."
-last_action: "Proof + stdlib wave 2026-06-01 → 02 landed (13 PRs): canonical-forms L1 modality-polymorphic (#274, P43, 7 lemmas axiom-free, prerequisite for progress_l1/P42); Print Assumptions audit framework across L1 + L3 keystones (#270, closes P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (#280, P06, HARD cases blocked on #240/#241/#242); Rust↔Coq is_linear_ty truth-table mechanical assertion (#273, P28); OwnershipKind from_byte/to_byte round-trip (#277, P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions as linear scopes (#275, D04), Allen's interval algebra (#272, D11), MessageHandle as linear typestate (#279, D17), monoidal aggregates (#281, D18); doc truth-restore + banned-preservation framing buried (#263); cluster-D L3/L4 status meander (#278); Track C panic-attack triage (#271); coq-build noble apt CI fix (#282, unblocks ~5 PRs); R5b standards SHA bump (#276). Plus CHANGELOG sync (#283). Build oracle clean across all 12 .v files. Print Assumptions: canonical_*_l1_m + most new lemmas zero-axiom; expected residuals (preservation_l1, region_liveness_at_split_l1_gen, region_shrink_preserves_typing_l1_gen_m) tracked. Stages 2-4 (#240/#241/#242) still un-touched. Wiki Proof-status.md refreshed 2026-06-02."
-updated: 2026-06-02T13:30:00Z
+last_action: "Proof + stdlib wave 2026-06-01 → 02 landed (13 PRs): canonical-forms L1 modality-polymorphic (#274, P43, 7 lemmas axiom-free, prerequisite for progress_l1/P42); Print Assumptions audit framework across L1 + L3 keystones (#270, closes P10/P32); step_pop_disjoint_from_type_l1 stated + EASY cases Qed-closed (#280, P06, HARD cases blocked on #240/#241/#242); Rust↔Coq is_linear_ty truth-table mechanical assertion (#273, P28); OwnershipKind from_byte/to_byte round-trip (#277, P59, typed-wasm ADR-0002 carrier handshake); 4 stdlib DB-theory additions — Transactions as linear scopes (#275, D04), Allen's interval algebra (#272, D11), MessageHandle as linear typestate (#279, D17), monoidal aggregates (#281, D18); doc truth-restore + banned-preservation framing buried (#263); cluster-D L3/L4 status meander (#278); Track C panic-attack triage (#271); coq-build noble apt CI fix (#282, unblocks ~5 PRs); R5b standards SHA bump (#276). Plus CHANGELOG sync (#283). Build oracle clean across all 12 .v files. Print Assumptions: canonical_*_l1_m + most new lemmas zero-axiom; expected residuals (preservation_l1, region_liveness_at_split_l1_gen, region_shrink_preserves_typing_l1_gen_m) tracked. Stages 2-4 (#240/#241/#242) still un-touched. Wiki Proof-status.md refreshed 2026-06-02. | INFRA (2026-06-24, non-proof track): governance docs landed (#314 — CODEOWNERS/GOVERNANCE.adoc/MAINTAINERS.adoc); standards reusable-workflow pins remediated (#315) and current at d135b05 (#316); Hypatia neurosymbolic gate now active and reporting 37 pre-existing findings (5 crit / 7 high / 25 med) — triage handed off (docs/governance/HYPATIA-HANDOFF.md), standards visibility patch drafted-not-applied. No .v files touched; no proof-state change."
+updated: 2026-06-24T18:13:15Z
 
 @directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
 # Captured durable directive — preservation work is the four-layer redesign,

@@ -7,6 +7,30 @@ All notable changes to Ephapax are documented here.
 
 ## [Unreleased]
 
+### Governance, CI & security-scan infrastructure (2026-06-24)
+
+- **Governance model formalised** (PR #314): added `.github/CODEOWNERS`
+  (review routing, sole-maintainer model), `GOVERNANCE.adoc`, and
+  `MAINTAINERS.adoc`. Salvaged from the closed estate-standardization
+  branch onto a clean base; prose headers normalised to `CC-BY-SA-4.0`.
+- **`standards` reusable-workflow pins remediated** (PR #315): re-pinned
+  `governance.yml` / `hypatia-scan.yml` / `scorecard.yml` away from
+  `5a93d9d57cc0` — a ref that is **not** an ancestor of `standards` HEAD,
+  which broke `governance / Check Workflow Staleness` and made the Hypatia
+  reusable workflow reference a dead `actions/cache` SHA — to a published
+  HEAD. Subsequently bumped to the current `d135b05…` (PR #316).
+- **Hypatia neurosymbolic scan unblocked** — with the pin fixed, the
+  `scan / Hypatia Neurosymbolic Analysis` gate now runs to completion
+  instead of dying at "Prepare all required actions". It reports **37
+  pre-existing findings** (5 critical, 7 high, 25 medium) — repo debt the
+  broken pin had been masking, **not** introduced here. Triage + fix is
+  **handed off** (see `docs/governance/HYPATIA-HANDOFF.md`); a visibility
+  patch for `standards`' `hypatia-scan-reusable.yml` (publish findings on
+  failure rather than aborting opaquely under `bash -e`) is **drafted but
+  not yet applied**.
+- **Stale PRs closed**: #310 (disjoint history; reintroduced fenced legacy
+  preservation work) and #311 (superseded — features already on `main`).
+
 ### Proof + stdlib wave (2026-06-01 → 2026-06-02)
 
 - **P43 — canonical-forms L1 modality-polymorphic** (PR #274): port

@@ -0,0 +1,98 @@
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
+<!-- Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+
+# Hypatia findings — outstanding triage handoff (2026-06-24)
+
+> **Status: OPEN.** The Hypatia neurosymbolic gate is now active and reports
+> **37 pre-existing findings (5 critical, 7 high, 25 medium)** on ephapax.
+> They are **not** fixed — triage + fix is the work below. These are
+> pre-existing repo debt that a broken CI pin had been masking, **not**
+> introduced by the change that unmasked them.
+
+## How this surfaced
+
+The `scan / Hypatia Neurosymbolic Analysis` gate used to die at "Prepare all
+required actions" because the three `hyperpolymath/standards` reusable
+workflows were pinned to `5a93d9d57cc0`, a ref that is **not** an ancestor of
+`standards` HEAD; that broken pin also transitively referenced a dead
+`actions/cache` SHA. PR #315 re-pinned to a published HEAD (later bumped to
+`d135b05…` in #316), which let the scan actually run — and report the 37
+findings that were previously invisible.
+
+> **Two milestones are not one:** "the workflow now *runs*" and "the workflow
+> now *passes*" are different. Fixing the pin achieved the first; the second
+> is this document.
+
+## Why this is handed off (cannot be run in the remote sandbox)
+
+The engine is an Elixir escript in `github.com/hyperpolymath/hypatia`. Building
+it needs `mix deps.get`, which fetches from **`repo.hex.pm`** — and the remote
+session's egress policy returns `403` for the Hex registry (npm/PyPI/crates/Go
+are allowed; Hex is not). So the engine must be run on a host where Hex is
+reachable (a local machine, or a CI runner), **or** the environment's network
+policy must be widened to allow `repo.hex.pm` + `builds.hex.pm`.
+
+## Task 1 — produce the exact findings
+
+```bash
+git clone https://github.com/hyperpolymath/hypatia.git ~/hypatia
+cd ~/hypatia
+mix local.hex --force && mix local.rebar --force
+mix deps.get
+mix escript.build
+# Run with NO GITHUB_TOKEN to match CI (CI had none, so the dependabot /
+# secret-scanning / code-scanning alert rules emit nothing — the 37 are
+# file-based rules):
+HYPATIA_FORMAT=json ./hypatia-cli.sh scan /path/to/ephapax > hypatia-findings.json
+jq '[.[].severity] | group_by(.) | map({(.[0]): length}) | add' hypatia-findings.json
+```
+
+- Rules are pure functions in `lib/rules/*.ex`; `scan` runs `@all_rule_modules`.
+- With no token the 37 are file-based — most likely from `honest_completion`,
+  `proof_obligation`, `disambiguation_rules`, `code_safety`, `root_hygiene`,
+  `supply_chain`, `structural_drift`, `workflow_audit`, `workflow_hardening`,
+  `cicd_rules`, `scorecard_compliance`. (A local token may surface MORE than
+  37 — run without one to reproduce the gate's set.)
+- Severities depend on the pinned `standards` reusable-workflow version
+  (currently `d135b05…`); the 5/7/25 split was observed on the first
+  unblocked run and may shift slightly with the engine version.
+
+## Task 2 — triage + fix
+
+1. Group by rule × severity. Fix order: **5 critical → 7 high → 25 medium**.
+2. Per finding: true positive → fix in code/docs; false positive / accepted →
+   add a justified `rule:path` line to `.hypatia-ignore` (matched `grep -qxF`),
+   or enter it in `.hypatia-baseline.json` (schema in `standards`
+   `.machine_readable/hypatia-baseline.schema.json`).
+3. **Proof / claim findings** (`honest_completion`, `proof_obligation`): fix by
+   making *claims* honest (docs/metadata), **never** by editing or force-closing
+   the fenced legacy proofs. Per `CLAUDE.md`: do not touch
+   `formal/Semantics.v` `Theorem preservation` (provably false; deliberately
+   `Admitted`), `formal/Typing.v`, or `formal/Counterexample.v`.
+4. **`disambiguation_rules`** findings: ensure the ephapax-vs-AffineScript
+   disambiguation markers are present per `CLAUDE.md`.
+5. Re-run the scan until `critical = 0` (ideally total within policy). Open a
+   PR with a triage table: *finding → disposition → fix*.
+
+## Task 3 — make the gate non-opaque (in `hyperpolymath/standards`)
+
+The gate fails **opaquely**: in `standards`'
+`.github/workflows/hypatia-scan-reusable.yml` the scan runs under `bash -e`,
+and `hypatia-cli.sh scan` **exits 1 when findings exist**, so the step aborts
+*before* the (already-present) `upload-artifact` step and the "warn but don't
+fail" critical-check ever run. Net effect: a hard job failure emitting only a
+severity count, no detail.
+
+**Fix (in `standards`):** wrap the scan in `set +e` + capture the rc; **always**
+upload `hypatia-findings.json` (`if: always()`); write a findings table to
+`$GITHUB_STEP_SUMMARY`; enforce the gate in a final dedicated step. Pin
+`actions/upload-artifact` by SHA (same supply-chain lesson as PR #315). A full
+suggested patch was drafted in-session (not yet applied).
+
+## Guardrails (from `CLAUDE.md`)
+
+- This is `hyperpolymath/ephapax` (not AffineScript). Signed commits.
+- Code/config = `MPL-2.0`; prose (`.md`/`.adoc`) = `CC-BY-SA-4.0`.
+- Never touch the fenced legacy preservation proof or `Typing.v` /
+  `Counterexample.v`. Fix proof/claim findings by aligning claims to reality.
@@ -77,6 +77,7 @@ The four layers and their current state:
 
 ## Governance
 
+- **Governance model**: sole-maintainer — [GOVERNANCE.adoc](https://github.com/hyperpolymath/ephapax/blob/main/GOVERNANCE.adoc), [MAINTAINERS.adoc](https://github.com/hyperpolymath/ephapax/blob/main/MAINTAINERS.adoc), [CODEOWNERS](https://github.com/hyperpolymath/ephapax/blob/main/.github/CODEOWNERS)
 - **Licence**: MPL-2.0
 - **Machine-readable state**: [`.machine_readable/6a2/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/6a2/)
 - **Contractiles**: 6-verb governance in [`.machine_readable/contractiles/`](https://github.com/hyperpolymath/ephapax/tree/main/.machine_readable/contractiles/)