hyperpolymath · hyperpolymath · Jun 21, 2026 · Jun 21, 2026 · Jun 21, 2026
@@ -1,4 +1,5 @@
-# SPDX-License-Identifier: PMPL-1.0
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: CC-BY-SA-4.0
 name: Scorecards supply-chain security
 on:
   branch_protection_rule:

@@ -1,4 +1,5 @@
-# SPDX-License-Identifier: PMPL-1.0
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: CC-BY-SA-4.0
 name: Secret Scanner
 on:
   pull_request:

@@ -5,9 +5,9 @@
 [metadata]
 project = "phronesis"
 version = "0.9.0"
-last-updated = "2026-06-20"
+last-updated = "2026-06-21"
 status = "active"
-session = "docs refresh + RSR/bot-doc compliance + root cleanup — 2026-06-20"
+session = "licensing dual-header standard + closeout triage (issues #59, #60) — 2026-06-21"
 
 [project-context]
 name = "Phronesis"
@@ -37,11 +37,13 @@ issues = [
 
 [critical-next-actions]
 actions = [
+  "Complete the dual-SPDX-header migration repo-wide (issue #59)",
+  "Wiki overhaul: audience-divided dev/maintainer/user + depth + re-frame (issue #60)",
   "Wire reflexion claim ingest for the compiler, formal/proof, and benchmark sources",
   "Advance the Rust to WASM production compiler beyond AST scaffolding",
   "Add Idris2 ABI definitions and the Zig FFI layer",
 ]
 
 [maintenance-status]
-last-run-utc = "2026-06-20T00:00:00Z"
+last-run-utc = "2026-06-21T00:00:00Z"
 last-result = "pass"  # unknown | pass | warn | fail  (full ExUnit suite green; consensus/Raft cases skipped pending :ra)
@@ -1,27 +1,22 @@
 # SPDX-License-Identifier: MPL-2.0
+# SPDX-License-Identifier: CC-BY-SA-4.0
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
 #
 # Machine-readable form of LICENSING.adoc. Tools enforce from this; humans read
 # the .adoc (the .adoc is the source of truth — keep in sync, do not diverge).
-# NOT a REUSE per-file dep5 map: this encodes the RULES, not per-file claims.
 
 schema = "hyperpolymath.licensing-policy/1"
 repo = "hyperpolymath/phronesis"
 classification = "sole-owner"            # estate category 1
 revised = "2026-06-21"
 human-source = "LICENSING.adoc"
 upstream-canonical = "hyperpolymath/standards: LICENCE-POLICY.adoc + .claude/CLAUDE.md §License Policy"
-note = "Sole-owner repo: code = MPL-2.0, prose docs = CC-BY-SA-4.0 (owner ruling 2026-06-04). Not a PMPL/AGPL/007 case. No automated/bulk SPDX edits."
+note = "Dual-licensed: every source file carries BOTH MPL-2.0 and CC-BY-SA-4.0 SPDX lines. Root LICENSE is MPL-2.0 (GitHub community-health marker). No automated/bulk SPDX edits."
 
-[default]                                # code/config/scripts/build/metadata/specs
-spdx = "MPL-2.0"
-scope = "*.ex, *.exs, *.rs, *.idr, *.tla, *.scm, mix.exs, Justfile, Mustfile, *.a2ml, *.toml"
-status = "the stated, legally-operative standard for code"
-
-[default_docs]                           # prose documentation
-spdx = "CC-BY-SA-4.0"
-scope = "narrative *.adoc and *.md (README, EXPLAINME, AUDIT, docs/, wiki/, academic/ prose)"
-status = "owner ruling 2026-06-04 — docs are CC-BY-SA-4.0; code stays MPL-2.0"
+[standard]                               # the per-file rule
+spdx = ["MPL-2.0", "CC-BY-SA-4.0"]
+form = "two SPDX-License-Identifier lines per file, in the file's comment syntax"
+scope = "all estate-authored source — code, config, build, workflows, formal specs/proofs, metadata, and prose docs"
 
 [github_marker]                          # GitHub community-health / 'git health'
 file = "LICENSE"
@@ -31,7 +26,6 @@ note = "root LICENSE carries plain MPL-2.0 text; GitHub detects one licence —
 [platform_exception]                     # registries
 spdx = "MPL-2.0"
 applies = "Hex / crates.io and other OSI-only registries; mix.exs package licenses = [MPL-2.0]"
-note = "explicit MPL-2.0 is compliance, not preference"
 
 [third_party]
 rule = "preserve original SPDX exactly; never relicense; flag-not-edit"
@@ -45,8 +39,8 @@ pmpl_carveout = "PMPL is exactly 3 repos (palimpsest-license, palimpsest-plasma,
 [automation]                             # estate Addendum A2
 allowed = false
 rule = "no bulk/sed/script/agent licence-SPDX changes; remediation is manual, per-file, owner-only"
-exception = "an agent may author NEW files with correct SPDX from birth"
+exception = "an agent may author NEW files with the correct dual header from birth"
 
-[flagged]                                # known deviations — owner-only to resolve, NOT swept
-apache_proofs = "academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/Phronesis.lean, lean4/lakefile.lean} carry Apache-2.0 (Lean/Coq/Agda ecosystem convention vs MPL-2.0 estate default — owner decision)"
-pmpl_workflows = ".github/workflows/{scorecard.yml, secret-scanner.yml} carry PMPL-1.0 — drift (not a carve-out repo); owner-only flip to MPL-2.0"
+[migration]                              # dual-header rollout
+done = "academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/*.lean}; .github/workflows/{scorecard,secret-scanner}.yml (previously Apache-2.0-OR-MIT and PMPL-1.0)"
+pending = "remaining single-SPDX estate files migrate to the dual header incrementally; mixed single/dual is owner-sanctioned during transition"
@@ -1,96 +1,74 @@
+// SPDX-License-Identifier: MPL-2.0
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = Phronesis — Licensing
 :toc:
 :icons: font
 
 The standard, authoritative statement of how Phronesis is licensed. Phronesis is
-a sole-owner hyperpolymath repository, so it follows the estate default: a
-*dual* licence — code under MPL-2.0, prose documentation under CC-BY-SA-4.0.
+a sole-owner hyperpolymath repository, dual-licensed: every source file is
+offered under *both* MPL-2.0 and CC-BY-SA-4.0.
 
 This document is the human source of truth; `.machine_readable/licensing-policy.toml`
-is its machine-readable twin (tools enforce from the TOML, humans read this —
-keep them in sync). The canonical estate policy is
-https://github.com/hyperpolymath/standards[`standards`] `LICENCE-POLICY.adoc`
-and `.claude/CLAUDE.md` §License Policy; this file is the Phronesis-local
-instance of it.
+is its machine-readable twin (keep them in sync). The canonical estate policy is
+https://github.com/hyperpolymath/standards[`standards`] `LICENCE-POLICY.adoc`.
 
-== The standard (dual labelling)
+== The standard — dual SPDX header on every file
 
-Two SPDX identifiers are in normal use across the repository — one per file,
-by file class:
+Every source file carries *two* SPDX identifier lines, in the file's comment
+syntax:
 
 [source]
 ----
-# Code, configuration, scripts, build files, A2ML metadata, formal specs:
 SPDX-License-Identifier: MPL-2.0
-
-# Prose documentation (*.adoc, narrative *.md):
 SPDX-License-Identifier: CC-BY-SA-4.0
 ----
 
 MPL-2.0 (file-level copyleft) keeps the implementation free and open even in
-networked deployments; CC-BY-SA-4.0 opens the documentation and research content
-under attribution and share-alike. Both licence texts live in `LICENSES/`
+networked deployments; CC-BY-SA-4.0 opens the same content for documentation and
+research reuse under attribution and share-alike. Both texts live in `LICENSES/`
 (`MPL-2.0.txt`, `CC-BY-SA-4.0.txt`), REUSE-style.
 
-== GitHub marker
-
-The root `LICENSE` file carries the plain *MPL-2.0* text. That is deliberate:
-it is the single licence GitHub detects for the repository's community-health
-profile ("git health") and the licence shown in the sidebar and API. CC-BY-SA-4.0
-is declared per-file and in `LICENSES/`, not in the root `LICENSE` (GitHub
-detects one). The distributed Hex package (`mix.exs`) also declares
-`licenses: ["MPL-2.0"]` — the code artefact.
-
-== Mapping
+This applies to all estate-authored source — `*.ex`, `*.exs`, `*.rs`, `*.idr`,
+`*.tla`, `*.agda`, `*.v`, `*.lean`, `*.scm`, `*.a2ml`, `*.toml`, build files,
+workflows, and prose docs (`*.adoc`, narrative `*.md`) alike.
 
-[cols="2,1,3"]
-|===
-| File class | SPDX | Examples
+== GitHub marker (community health)
 
-| Source code | `MPL-2.0` | `*.ex`, `*.exs`, `*.rs`, `*.idr`
-| Formal specs / semantics | `MPL-2.0` | `*.tla`, `spec/SPEC.core.scm`
-| Build / config / metadata | `MPL-2.0` | `mix.exs`, `Justfile`, `Mustfile`, `*.a2ml`, `*.toml`
-| Prose documentation | `CC-BY-SA-4.0` | `README.adoc`, `EXPLAINME.adoc`, `AUDIT.adoc`, `docs/**`, `wiki/**`, `academic/**` prose
-| Root licence text | `MPL-2.0` | `LICENSE` (GitHub marker)
-|===
+The root `LICENSE` file carries the plain *MPL-2.0* text. That is the single
+licence GitHub detects for the repository's community-health profile ("git
+health") and shows in the sidebar and API. The dual per-file labelling above is
+declared in headers and in `LICENSES/`; the root `LICENSE` stays MPL-2.0 so the
+community-health marker is MPL-2.0. The distributed Hex package (`mix.exs`) also
+declares `licenses: ["MPL-2.0"]`.
 
 == Exclusion cases
 
-The dual standard above is the *normal*. It does not apply in these cases:
-
-* *Third-party / vendored* (`deps/**`, any upstream code): preserve the
-  original SPDX exactly — flag, never edit or relicense.
-* *Platform registries* (Hex, crates.io): an explicit `MPL-2.0` declaration is
-  a compliance requirement, not a preference.
-* *Not applicable to Phronesis:* the estate's other categories — All-Rights-Reserved
-  (`007`), `AGPL-3.0-or-later` (repos shared with the owner's son), and
-  `PMPL-1.0-or-later` (the three Palimpsest carve-out repos only) — do **not**
-  apply here. Phronesis is a plain sole-owner repo.
-
-== Known deviations (flagged, owner-only to resolve)
-
-Per estate policy, licence-SPDX changes are *manual, per-file, owner-only* — no
-bulk or automated edits (see `standards` `LICENCE-POLICY.adoc` Addendum A2 and
-the neurophone#99 post-mortem). The following currently deviate from the
-standard and are recorded here for an owner decision rather than swept:
-
-[cols="2,1,3"]
-|===
-| Files | Current SPDX | Note
-
-| `academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/Phronesis.lean, lean4/lakefile.lean}` (5)
-| `Apache-2.0`
-| Estate-authored proof files. Apache-2.0 is the convention of the Lean/Coq/Agda
-  proof ecosystems; confirm whether to keep (ecosystem convention) or normalise
-  to `MPL-2.0` (estate default for code).
-
-| `.github/workflows/{scorecard.yml, secret-scanner.yml}` (2)
-| `PMPL-1.0`
-| Drift — Phronesis is not a Palimpsest carve-out repo, so these workflow files
-  should be `MPL-2.0`. PMPL flips are owner-only; not auto-changed.
-|===
+The dual standard is the *normal*. It does not apply to:
+
+* *Third-party / vendored* (`deps/**`, any upstream code): preserve the original
+  SPDX exactly — flag, never edit or relicense.
+* *The root `LICENSE` file*: the verbatim MPL-2.0 text (the GitHub marker), not a
+  dual-headed source file.
+* *Not applicable to Phronesis:* the estate's other categories — ARR (`007`),
+  `AGPL-3.0-or-later` (son-shared repos), `PMPL-1.0-or-later` (the three
+  Palimpsest carve-out repos only) — do not apply here.
+
+== Migration status
+
+The dual-header standard is being rolled out per-file (manual, owner-directed —
+no bulk/automated SPDX sweeps, per `standards` `LICENCE-POLICY.adoc` Addendum A2
+and the neurophone#99 post-mortem).
+
+* *Done:* the formal-verification proof files
+  (`academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/*.lean}`)
+  and the two affected workflows
+  (`.github/workflows/{scorecard.yml, secret-scanner.yml}`) now carry the dual
+  header (previously `Apache-2.0 OR MIT` and `PMPL-1.0` respectively).
+* *Pending:* the remaining estate-authored files that still carry a single SPDX
+  line are migrated to the dual header incrementally. Until then the repository
+  legitimately mixes single- and dual-headed files; both are owner-sanctioned
+  during the transition.
 
 == See also
 

@@ -1,4 +1,5 @@
--- SPDX-License-Identifier: Apache-2.0 OR MIT
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-License-Identifier: CC-BY-SA-4.0
 -- Phronesis Formalization in Agda
 -- Intrinsically typed representation with dependent types
 

@@ -1,4 +1,5 @@
--- SPDX-License-Identifier: Apache-2.0 OR MIT
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-License-Identifier: CC-BY-SA-4.0
 -- Copyright (c) 2026 Jonathan D.A. Jewell
 --
 -- =====================================================================

@@ -1,4 +1,5 @@
-(* SPDX-License-Identifier: Apache-2.0 OR MIT *)
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* SPDX-License-Identifier: CC-BY-SA-4.0 *)
 (* Phronesis Formalization in Coq *)
 (* Complete mechanized proofs of type safety, termination, and security properties *)
 

@@ -1,4 +1,5 @@
--- SPDX-License-Identifier: Apache-2.0 OR MIT
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-License-Identifier: CC-BY-SA-4.0
 -- Phronesis Formalization in Lean 4
 -- Mechanized proofs of type safety, termination, and security properties.
 --

@@ -1,4 +1,5 @@
--- SPDX-License-Identifier: Apache-2.0 OR MIT
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-License-Identifier: CC-BY-SA-4.0
 -- Minimal Lake build for the Phronesis Lean 4 metatheory.
 -- No external dependencies (no Mathlib): builds on core Lean only, so CI
 -- needs nothing but the toolchain pinned in `lean-toolchain`.