fix(licence): canonicalise to PMPL-1.0-or-later per authorship check (#133)

hyperpolymath · claude · hyperpolymath · commit 40044ad39c85 · 2026-05-19T21:19:17.000+01:00
Refs hyperpolymath/standards#133 / standards#124. NOT Closes (proof-debt — main soundness/rescue-branch — is separate). Authorship check (git shortlog + per-file git log): every affected file is 100% owner-own (Jonathan D.A. Jewell); dependabot touched only CI; nothing vendored/third-party; no AGPL-by-intent. The "AGPL-3.0 / Palimpsest 0.5" strings are scaffold-placeholder drift (the ledger root cause), not a deliberate election. Owner-ruled. - 13 proof files: `License: AGPL-3.0 / Palimpsest 0.5` -> `License: PMPL-1.0-or-later` (matches the 2 already-correct files CNOCategory.v / LambdaCNO.v; ledger rule #5 + stale-Palimpsest->PMPL). - 4 missing-header files (owner-own): added the canonical header — StatMech_helpers.v in the repo proof-file doc-comment form (Author/Project/License), src/main.rs + src/brainfuck/src/main.rs + src/AuditTrail.res with the estate SPDX+Copyright form (CLAUDE.md requires SPDX headers on all files). - Deleted the 0-byte LICENSE-PALIMPS.txt stub: NOT referenced by root LICENSE (which references EXHIBIT-A/B), and the repo's own audit trail (LICENSE-AUDIT-2026-02-05.adoc, ROADMAP, SESSION-COMPLETE) already prescribes its removal. Canonical text remains in license/PMPL-1.0.txt and root LICENSE. Header-only; no proof semantics touched (build/soundness state is the separate standards#133 proof-debt item — the unmerged rescue branch). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/LICENSE-PALIMPS.txt b/LICENSE-PALIMPS.txt
diff --git a/proofs/coq/common/CNO.v b/proofs/coq/common/CNO.v
@@ -5,7 +5,7 @@
 
     Author: Jonathan D. A. Jewell
     Project: Absolute Zero
-    License: AGPL-3.0 / Palimpsest 0.5
+    License: PMPL-1.0-or-later
 *)
 
 Require Import Coq.Init.Nat.
diff --git a/proofs/coq/filesystem/FilesystemCNO.v b/proofs/coq/filesystem/FilesystemCNO.v
@@ -15,7 +15,7 @@
 
     Author: Jonathan D. A. Jewell
     Project: Absolute Zero (integrating Valence Shell)
-    License: AGPL-3.0 / Palimpsest 0.5
+    License: PMPL-1.0-or-later
 *)
 
 Require Import Coq.Lists.List.
diff --git a/proofs/coq/malbolge/MalbolgeCore.v b/proofs/coq/malbolge/MalbolgeCore.v
@@ -7,7 +7,7 @@
 
     Author: Jonathan D. A. Jewell
     Project: Absolute Zero
-    License: AGPL-3.0 / Palimpsest 0.5
+    License: PMPL-1.0-or-later
 *)
 
 Require Import CNO.CNO.
diff --git a/proofs/coq/physics/LandauerDerivation.v b/proofs/coq/physics/LandauerDerivation.v
@@ -7,7 +7,7 @@
 
     Author: Jonathan D. A. Jewell
     Project: Absolute Zero - Phase 1 Complete Derivation
-    License: AGPL-3.0 / Palimpsest 0.5
+    License: PMPL-1.0-or-later
 *)
 
 Require Import Coq.Reals.Reals.
diff --git a/proofs/coq/physics/StatMech.v b/proofs/coq/physics/StatMech.v
@@ -6,7 +6,7 @@
 
     Author: Jonathan D. A. Jewell
     Project: Absolute Zero
-    License: AGPL-3.0 / Palimpsest 0.5
+    License: PMPL-1.0-or-later
 *)
 
 Require Import Coq.Reals.Reals.
diff --git a/proofs/coq/physics/StatMech_helpers.v b/proofs/coq/physics/StatMech_helpers.v
@@ -2,6 +2,10 @@
 
     Auxiliary lemmas needed for thermodynamic CNO proofs.
     These should eventually be integrated into CNO.v.
+
+    Author: Jonathan D. A. Jewell
+    Project: Absolute Zero
+    License: PMPL-1.0-or-later
 *)
 
 Require Import CNO.
diff --git a/proofs/coq/quantum/QuantumCNO.v b/proofs/coq/quantum/QuantumCNO.v
@@ -12,7 +12,7 @@
 
     Author: Jonathan D. A. Jewell
     Project: Absolute Zero
-    License: AGPL-3.0 / Palimpsest 0.5
+    License: PMPL-1.0-or-later
 *)
 
 Require Import Coq.Reals.Reals.
diff --git a/proofs/coq/quantum/QuantumMechanicsExact.v b/proofs/coq/quantum/QuantumMechanicsExact.v
@@ -8,7 +8,7 @@
 
     Author: Jonathan D. A. Jewell
     Project: Absolute Zero - Exact Quantum Formulation
-    License: AGPL-3.0 / Palimpsest 0.5
+    License: PMPL-1.0-or-later
 *)
 
 Require Import Coq.Reals.Reals.
diff --git a/proofs/lean4/CNO.lean b/proofs/lean4/CNO.lean
@@ -5,7 +5,7 @@
 
    Author: Jonathan D. A. Jewell
    Project: Absolute Zero
-   License: AGPL-3.0 / Palimpsest 0.5
+   License: PMPL-1.0-or-later
 -/
 
 -- Std.Data.{List,Nat}.Basic were vestigial: Std was renamed to Batteries
diff --git a/proofs/lean4/CNOCategory.lean b/proofs/lean4/CNOCategory.lean
@@ -5,7 +5,7 @@
 
    Author: Jonathan D. A. Jewell
    Project: Absolute Zero
-   License: AGPL-3.0 / Palimpsest 0.5
+   License: PMPL-1.0-or-later
 -/
 
 import CNO
diff --git a/proofs/lean4/FilesystemCNO.lean b/proofs/lean4/FilesystemCNO.lean
@@ -5,7 +5,7 @@
 
    Author: Jonathan D. A. Jewell
    Project: Absolute Zero (integrating Valence Shell)
-   License: AGPL-3.0 / Palimpsest 0.5
+   License: PMPL-1.0-or-later
 -/
 
 -- Std.Data.List.Basic was vestigial in pre-Batteries layouts. The List
diff --git a/proofs/lean4/LambdaCNO.lean b/proofs/lean4/LambdaCNO.lean
@@ -7,7 +7,7 @@
 
    Author: Jonathan D. A. Jewell
    Project: Absolute Zero
-   License: AGPL-3.0 / Palimpsest 0.5
+   License: PMPL-1.0-or-later
 -/
 
 namespace LambdaCNO
diff --git a/proofs/lean4/QuantumCNO.lean b/proofs/lean4/QuantumCNO.lean
@@ -5,7 +5,7 @@
 
    Author: Jonathan D. A. Jewell
    Project: Absolute Zero
-   License: AGPL-3.0 / Palimpsest 0.5
+   License: PMPL-1.0-or-later
 -/
 
 import Mathlib.Data.Real.Basic
diff --git a/proofs/lean4/StatMech.lean b/proofs/lean4/StatMech.lean
@@ -5,7 +5,7 @@
 
    Author: Jonathan D. A. Jewell
    Project: Absolute Zero
-   License: AGPL-3.0 / Palimpsest 0.5
+   License: PMPL-1.0-or-later
 -/
 
 import CNO
diff --git a/src/AuditTrail.res b/src/AuditTrail.res
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 // AuditTrail.res - DOM annotation for debugging
 // Injects data-audit paths into the DOM
 
diff --git a/src/brainfuck/src/main.rs b/src/brainfuck/src/main.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Brainfuck CNO Detection CLI
 //!
 //! Tests various Brainfuck programs for CNO properties.
diff --git a/src/main.rs b/src/main.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Certified Null Operation in Rust
 //!
 //! A program that does absolutely nothing at the application level.
