Tranche A remediation + GNPL design documents (#6)

## What this is

`gnpl` was reserved as Lithoglyph's **narration/projection** language,
then filled by a
squash-import of the GQLdt *query* language from the
`nextgen-databases/lithoglyph/`
monorepo. The import was not a mistake — it faithfully executed a
migration plan that
defined GNPL narrowly, as a rename of "Glyph query language".

That reading is superseded. **Narration/projection is the primary
purpose**; practical
value to Lithoglyph-as-a-database is second. This PR encodes that, and
fixes the
remediation backlog that had accumulated behind a CI job which had never
actually run.

**Structure: two layers, one repo.** Nothing is extracted, nothing
discarded.

```
GNPL  ──lowers to──▶  GQLdt  ──FFI──▶  Lithoglyph
(what account)       (what is)        (the data store)
```

No `src/Gnpl/` code in this pass, by design — the skeleton is a
follow-up.

---

## Measured findings

Everything below was run, not inferred.

### `lake build` succeeds

Status was previously **unknown**, because CI died before reaching it.
Run locally with the
full-mathlib cost budgeted:

- exit 0, 34/35 targets, `Build completed successfully`
- **zero `sorry` warnings from Lean's own checker**, zero errors

This unblocks the deferred skeleton.

### CI was building the wrong Zig tree

`bridge/` builds clean on Zig 0.16 and emits
`zig-out/lib/liblith_bridge.a` — exactly the
artifact `lakefile.lean` links (`-Lbridge/zig-out/lib -llith_bridge`).

`bridge/zig/` **fails to compile its own build script**: it uses
`addStaticLibrary` and
`linkLibC`, removed from the Zig Build API after 0.14. CI had been
pointed at it. There are
three distinct skeletons in this repo — `bridge/`, `bridge/zig/`,
`ffi/zig/` — and only the
first is real.

### The build gate was never real

`actions/cache@0c45773b…` is deprecated and **hard-fails**, aborting the
job *before*
`lake build`. So a red ❌ on `Build and Test Lean 4` has never meant "the
Lean code is
broken" — it meant the cache action refused to start.

### The naming gate could only ever pass

```bash
grep -i "gql-dt" STATE.scm ECOSYSTEM.scm 2>/dev/null && echo "Found old naming (gql-dt instead of gql-dt)"
```

It compares a string to itself, over two files that do not exist, with
`2>/dev/null`
swallowing the miss. Deleted rather than repaired.

### The link checker was suppressing its own findings

`.github/markdown-link-check-config.json` carried an ignorePattern for
`^https://github.com/hyperpolymath/lith` — which silently exempted
**every** dead
`lith*` link in the repo. Verified via `gh`: `gql-dt`, `lith`,
`lithoglyph`,
`lithoglyph-studio`, `lithoglyph-debugger` **do not exist**. Narrowed to
`^http://localhost`.

### Licence clobber, with chronology

`git log -- LICENSE` shows only two commits ever touched it:

| Commit | Effect |
|---|---|
| `a144d9f` (2026-06-24) | "normalise to MPL-2.0 (code) + CC-BY-SA-4.0
(docs)" — verbatim MPL-2.0 |
| `102c79e` (the import) | **overwrote** it with PALIMPSEST-MPL 1.0,
carried in from the monorepo |

The result was an `SPDX-License-Identifier: MPL-2.0` header sitting
above a PMPL body — the
same header/body inversion previously found in `idaptik-ums`. All 50
code files already
declared MPL-2.0; only the docs and the vscode manifest dissented.

**And the clobber had a regeneration mechanism.**
`.machine_readable/6a2/AGENTIC.a2ml:22` instructed agents: *"Never use
AGPL license (use
PMPL-1.0-or-later)"*. Fixing `LICENSE` alone would have been undone by
the next agent pass.
That directive is now corrected.

PMPL is a real licence (`hyperpolymath/palimpsest-license`) — it is
simply not this repo's.
`LICENSE` restored verbatim from `a144d9f`.

---

## Changes

### Proof gate — `scripts/check-lean-proofs.sh` (new)

The old gate was `! grep -r "sorry\|admit" src/`. It fires on five
legitimate constructs in
this repo, none of which are incomplete proofs:

| Location | What it actually is |
|---|---|
| `TypeInference.lean:162` | `\| admit : ProofStrategy` — a
**constructor** |
| `TypeInference.lean:171` | `.admit` — a reference to it |
| `TypeInference.lean:179` | the string literal `"sorry"` |
| `TypeSafeQueries.lean:90` | a **commented-out** `:= by sorry` |
| `Lexer.lean:230` | `("sorry", .kwSorry)` — a keyword table entry |

Two modes:

- **`--build-log FILE` (authoritative)** — reads Lean's own diagnostics
(`uses '?sorry'?`, `sorryAx`, `declaration uses`). **Exits 1 if the log
is missing**; a
  gate must never report success from a file that does not exist.
- **default (textual pre-check)** — strips `/- -/` blocks, `"strings"`
and `--` comments
  before matching, and exempts constructor declarations.

**Canary-tested five ways, all correct:** current `src/` passes → seeded
`theorem canary_one : True := by sorry` fails → seeded `example : 1 = 1
:= by admit` fails
→ real build log passes → seeded warning log fails → missing log fails.
A gate that has
never gone red is not evidence of anything.

### CI — `.github/workflows/lean-build.yml`

- `actions/cache` → live v4 SHA (`5a3ec84e…`)
- `goto-bus-stop/setup-zig@2a9625d…` → `mlugg/setup-zig@d1434d08…`; the
old SHA does not
  exist and that action has **no v2 tag at all**
- `zig-ffi` repointed at `bridge/`, asserts
`zig-out/lib/liblith_bridge.a` exists, runs
  `zig build test` (dropped a nonexistent `test-integration` step)
- build step now `set -o pipefail; lake build 2>&1 | tee
lake-build.log`, feeds the log to
  the proof gate, and uploads it as an artifact
- spec filenames corrected to the real `spec/GQL-DT-Lexical.md` /
`GQL-DT-Railroad-Diagrams.md`
(a naming mismatch, not a missing spec) and now collect all misses
rather than exiting on
  the first
- tautological naming gate deleted

### Identity

- **`README.adoc`** was the unmodified RSR template — *"This is your
repo - don't forget to
rename me!"*. Rewritten to lead with the two-layer story, so a visitor
immediately
  understands why a repo named `gnpl` contains code namespaced `GqlDt`.
- **`MOVED.md`** removed. It claimed this content moved *to*
`hyperpolymath/lith` — a repo
  that does not exist, and the reverse of what happened.
- `gqldt.ipkg`, `0-AI-MANIFEST.a2ml`, `META.a2ml` repointed at
`github.com/hyperpolymath/gnpl`.

### Toolchains — `mise.toml` (new)

Declares what this repo actually uses: `zig = "0.16.0"`, `idris2`, per
the estate ABI
(Idris2) / FFI (Zig) standard. Lean is **deliberately not pinned here**
— `lean-toolchain`
(`leanprover/lean4:v4.15.0`) is the single source of truth and elan
reads it; a second pin
would be a second thing to drift.

---

## Design documents

### `docs/THEORY.adoc` — the untethered case

What a narration/projection language is and what gap it fills. It
credits each neighbour
and says precisely where it stops:

| Neighbour | Where it stops |
|---|---|
| Bitemporal DBs (SQL:2011, Datomic, XTDB) | one consistent world *per
coordinate*; two irreconcilable witnesses remain a data-quality defect |
| Provenance semirings (Green/Tannen; Buneman) | annotates *a result* —
"where did this tuple come from", not an account *of the matter* |
| Argumentation (Dung, ASPIC+, Dempster–Shafer) | reasoning formalisms,
not database languages; no narrative arrangement |
| AGM belief revision | belief *sets*, not accounts; silent on where
entrenchment comes from |
| Event / situation calculus | reasons about what follows from events
*taken as known*; no contested evidence, no perspective |
| Computational narratology | commitment is aesthetic, not evidential —
it may invent |
| Narratology (Genette) | descriptive literary theory; nothing
mechanised |

The claim is scoped, and **six novelty claims are explicitly
disclaimed**. The document
says outright: *GNPL is a synthesis, not a discovery.* Its value stands
or falls on whether
the synthesis is usable.

Governing invariant, mirroring GQLdt's existing rule at the data layer:

> **No narration without warrant.** The type system forbids constructing
an `Account`
> containing an assertion not derivable from its `Fabula` under the
stated `Focalization`.

Ends with seven open questions, so the deferred work starts from an
agenda rather than a
blank page.

### `docs/LITHOGLYPH.adoc` — the tethered case

Grounded in three facts verifiable in code, not asserted:

1. `Form.Blocks` maintains an append-only journal, with journal entries
written **before**
   block mutations (`lithoglyph/ARCHITECTURE.adoc`).
2. `Provenance/Rationale.lean` — *"you cannot construct a `Tracked`
value without providing
   a non-empty rationale"*, enforced at the type level.
3. `bridge/lith_types.zig` already marshals `ActorIdC`, `RationaleC`,
`ProvenanceC`,
   `TrackedValueC` across the C ABI.

**Three of six GNPL constructs already exist** — including the two
hardest to retrofit.
The argument from sunk cost: mandatory rationale is currently a *tax*
consumed by nothing,
and features like that get quietly filled with boilerplate. GNPL is the
consumer that makes
it pay.

It also flags a live hazard: `PromptScoresC.computeOverall` and
`Confidence.avg` are
**unweighted means**. Neither is probabilistically principled, and both
would be
load-bearing if used as an AGM entrenchment ordering. Must be resolved
before any
retraction result reaches a user.

---

## Out of scope — flagged, not fixed

- **Stale Zig skeletons.** `bridge/zig/` and `ffi/zig/` are
near-duplicates on the removed
pre-0.15 Build API; nothing links against either. Deleting them is a
separate call.
- **`RSR_OUTLINE.adoc`** still says "AGPL + Palimpsest dual license"
(lines 72, 160). That is
RSR *template* scaffolding describing the template standard, not this
repo's declaration.
- **Sibling extractions.** This clobber rode in on a routine
squash-import. Worth checking
whether `glyphbase` and the pending `lithoglyphdb` carry the same
PMPL-over-MPL overwrite.
- **Estate-shared CI.** `Governance` (scorecard-SARIF policy;
trusted-base "no
`docs/proof-debt.md` but 19 escape hatches") and `Hypatia` (`ImageOS`
`ubuntu24`
unmappable) are `hyperpolymath/standards` reusable-workflow issues.
Fixing them from
  inside `gnpl` would be papering over an upstream fault.

## Companion PR

A second PR against `hyperpolymath/nextgen-databases` corrects
`lithoglyph/MOVED.md`, which
claims `core-factor/gql/` was migrated here. It was not — that is 5
Factor files, and this
repo contains zero `.factor` files. The Factor half is being treated as
legacy and
superseded by a typed narration layer lowering to GQLdt, rather than
migrated.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---

# Update — corrections after verifying against the estate checkers

Two claims in the body above were wrong, and correcting them turned up
the most
significant finding in this PR. Recorded here rather than silently
edited.

## Correction 1: the Governance failures were **not** estate-shared

I listed Governance under "out of scope — upstream". I then cloned
`hyperpolymath/standards` and ran its checkers locally against this
repo. **Both Governance
failures are repo-local and fixable here.** Only Hypatia is genuinely
upstream.

Filed upstream, with evidence:
- **hyperpolymath/standards#516** — Hypatia: the pinned
`erlef/setup-beam` SHA cannot map
`ImageOS=ubuntu24`, so the scanner never runs *for any caller*.
SHA-pinning holding
  callers at a pre-fix revision.
- **hyperpolymath/standards#517** — `check-trusted-base.sh`: Lean
`\bsorry\b` matches
  string literals and keyword tables (low severity; no false *passes*).

## Correction 2: "no incomplete proofs" was true but **materially
incomplete**

The body above says Lean reports zero `sorry`. That is accurate and I
verified it in CI.
It is **not** the same as "the proofs are done", and I should not have
let it stand alone.

**Lean's `sorry` warning does not fire on `axiom`.** Running the estate
trusted-base
checker found **19 escape hatches — 16 real `axiom` declarations** (plus
the 3 detector
false positives in #517).

**None of the 16 is a necessary axiom.** Every one is a stub. Two
consequences:

**Five sit in executable position.** `parseToIR`, `deserializeIR`,
`many`, `many1`, `sepBy`
are declared `axiom`, so they have **no implementation at all**. Code
calling them
typechecks and cannot run. *"34/35 targets build" is a statement about
typechecking, not
about a working parser.*

**One is a vacuous soundness theorem.** `TypeSafe.lean:194`:

```lean
-- Proof that execution preserves type safety
-- Stubbed due to satisfiesConstraints signature issue
axiom executePreservesTypes {schema : Schema} (stmt : InsertStmt schema) :
  ∀ i, i < stmt.values.length →
    let ⟨_t, _v⟩ := stmt.values.get! i
    True  -- Placeholder
```

It reduces to `… → True`. It reads as a type-safety soundness theorem
and discharges
nothing. Marked **D1, close first** — the only item that *actively
misinforms*.

And the sharpest one: the `TypeSafeQueries.lean` worked examples — the
ones commented
`✓ Type-safe INSERT with valid score`, demonstrating that an
out-of-range score gives
`-- Type error: failed to prove 150 ≤ 100` — **are themselves axioms**.
They assert the
existence of the well-typed value rather than constructing it,
demonstrating the opposite
of what the comments claim.

None of this is a regression introduced here. It is the inherited state
of the imported
GQLdt sources, recorded honestly for the first time.

### `docs/proof-debt.md` (new)

All 19 enumerated with `file:line` under the policy schema — §(a)
discharged, §(b) budgeted,
§(c) necessary, §(d) debt, and an §(e) section for the detector false
positives so the count
reconciles (19 = 16 + 3). Grouped into four work items with plans: D1
the vacuous theorem,
D2 the unimplemented combinators, D3 the asserted examples (lowest
effort, highest
credibility gain — do first after D1), D4 the one item with a reasoned
justification.

**§(b) is deliberately empty and must stay empty until a test driver
exists.** Without a
refutation budget, "covered by tests" is unfalsifiable — the policy's
own point.

Checker now passes honestly: `All 19 escape hatch(es) are documented.`

### Scorecard SARIF — a real local violation

`Check Workflow Staleness` asserted: *"OSSF Scorecard must not upload
SARIF to GitHub Code
Scanning unless it runs for every PR head commit."* True here:
`scorecard.yml` triggers on
push-to-main/schedule/dispatch — **never `pull_request`** — yet ran
`github/codeql-action/upload-sarif`. Code Scanning would show findings
corresponding to no
PR head commit.

Scan retained, upload switched to a build artifact, `security-events:
write` dropped.
Verified locally: *"All workflow staleness checks passed."*

## Also fixed: a third gate that could not fail

The first CI run went green — and the log showed why that was not
entirely earned:

```
Run Lean tests   error: gqldt: no test driver configured
conclusion: success
```

The step was `lake test || echo "No tests configured yet"`. `lake test`
exits non-zero both
when tests **fail** and when no driver is configured; `|| echo`
swallowed both, so a real
test failure could never have turned the job red. Same shape as the
naming gate deleted
earlier in this PR.

Now a genuine failure exits 1, and only `no test driver configured` is
tolerated — surfaced
as a `::warning::` recording that **this repository has no executable
test coverage**,
rather than passing silently. Verified in CI: the `elif` branch is taken
and the annotation
is emitted.

## README

The status table said the core *"builds"*; it now says *"typechecks"*,
with added rows for
the 16 outstanding axioms and the absence of tests, and the proof-gate
section carries:

> A green proof gate here means "nothing is admitted mid-proof". It does
**not** mean
> "nothing is assumed."

`README.md` still opened with the pre-re-scope, query-first title,
contradicting
`README.adoc`. Confirmed via `gh api repos/hyperpolymath/gnpl/readme`
that GitHub renders
**`README.adoc`**, and `casket-pages.yml` prefers it too — so the
landing page was already
correct. `README.md` is reframed as the GQLdt-layer document with a
banner pointing at
`README.adoc`.

---------

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: hyperpolymath

.github/markdown-link-check-config.json

@@ -1,8 +1,5 @@
 {
   "ignorePatterns": [
-    {
-      "pattern": "^https://github.com/hyperpolymath/lith"
-    },
     {
       "pattern": "^http://localhost"
     }
@@ -11,5 +8,8 @@
   "retryOn429": true,
   "retryCount": 3,
   "fallbackRetryDelay": "30s",
-  "aliveStatusCodes": [200, 206]
+  "aliveStatusCodes": [
+    200,
+    206
+  ]
 }

.github/workflows/lean-build.yml

@@ -31,8 +31,11 @@ jobs:
           lean --version
           lake --version
 
+      # Was actions/cache@0c45773b… — a deprecated version that GitHub hard-fails.
+      # That failure aborted this job BEFORE `lake build` ever ran, which is why
+      # CI never once reported whether this project compiles.
       - name: Cache Lean dependencies
-        uses: actions/cache@0c45773b623bea8c8e75f6c82b208c3cf94ea4f9 # v4
+        uses: actions/cache@5a3ec84eff668545956fd18022155c47e93e2684 # v4.2.3
         with:
           path: |
             .lake
@@ -41,19 +44,44 @@ jobs:
           restore-keys: |
             ${{ runner.os }}-lean-
 
+      # Tee the build so the proof gate can read Lean's own diagnostics.
+      # pipefail so a build failure is not masked by the pipe into tee.
       - name: Build Lean 4 project
-        run: lake build
-
+        run: |
+          set -o pipefail
+          lake build 2>&1 | tee lake-build.log
+
+      # `lake test` exits non-zero BOTH when tests fail and when no test driver
+      # is configured. The previous step was `lake test || echo "..."`, which
+      # swallowed both — so a genuine test failure could never turn this job red.
+      # Tolerate only the "no test driver" case, and surface it as a warning
+      # rather than a silent pass: no driver means no executable test coverage.
       - name: Run Lean tests
-        run: lake test || echo "No tests configured yet"
-
-      - name: Check for proof errors
         run: |
-          echo "Checking for sorry/admit in proofs..."
-          ! grep -r "sorry\|admit" src/ || {
-            echo "❌ Found incomplete proofs (sorry/admit)"
+          set -o pipefail
+          if lake test 2>&1 | tee lake-test.log; then
+            echo "✅ lake test passed"
+          elif grep -q "no test driver configured" lake-test.log; then
+            echo "::warning::No Lean test driver is configured, so this repository has NO executable test coverage. Add a @[test_driver] to lakefile.lean."
+          else
+            echo "::error::lake test failed"
             exit 1
-          }
+          fi
+
+      # Authoritative proof gate. Lean itself emits "declaration uses 'sorry'";
+      # the previous gate was `! grep -r "sorry\|admit" src/`, which fired on a
+      # lexer keyword table, a string literal, a comment and two constructor
+      # references — and could not see a sorry reached through a tactic block.
+      - name: Check for incomplete proofs (authoritative)
+        run: ./scripts/check-lean-proofs.sh --build-log lake-build.log
+
+      - name: Upload build log
+        if: always()
+        uses: actions/upload-artifact@26f96dfa697d77e81fd5907df203aa23a56210a8 # v4
+        with:
+          name: lake-build-log
+          path: lake-build.log
+          retention-days: 30
 
   zig-ffi:
     name: Build Zig FFI Bridge
@@ -63,23 +91,34 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
 
+      # Was goto-bus-stop/setup-zig@2a9625d… — that SHA does not exist and the
+      # action is unmaintained (it has no v2 tag at all), so this job could
+      # never start. mlugg/setup-zig is the maintained successor.
       - name: Setup Zig
-        uses: goto-bus-stop/setup-zig@2a9625d550eefc3a8b5fe73f3f4ca4cf9b74d84c # v2
+        uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2
         with:
-          version: 0.13.0
+          version: 0.16.0
 
+      # Was `working-directory: bridge/zig`. That is a stale skeleton on the
+      # pre-0.15 Build API (`addStaticLibrary`, `linkLibC`) which no longer
+      # compiles, and nothing links against it. The real bridge is `bridge/`:
+      # `lakefile.lean` links `-Lbridge/zig-out/lib -llith_bridge`, and
+      # `bridge/build.zig` is what produces `liblith_bridge.a` at that path.
       - name: Build Zig bridge
-        working-directory: bridge/zig
+        working-directory: bridge
         run: zig build
 
+      - name: Verify the artifact Lean links against exists
+        working-directory: bridge
+        run: test -f zig-out/lib/liblith_bridge.a
+
+      # bridge/build.zig declares exactly two steps: "shared" and "test".
+      # The old workflow also ran `zig build test-integration`, which is not a
+      # step in any build.zig here and would always have failed.
       - name: Run Zig tests
-        working-directory: bridge/zig
+        working-directory: bridge
         run: zig build test
 
-      - name: Run integration tests
-        working-directory: bridge/zig
-        run: zig build test-integration
-
   spec-validation:
     name: Validate Specifications
     runs-on: ubuntu-latest
@@ -91,36 +130,36 @@ jobs:
       - name: Check EBNF grammar syntax
         run: |
           echo "Validating EBNF grammar..."
-          # Basic validation - check for balanced brackets
           if ! grep -E '::=' spec/GQLdt-Grammar.ebnf > /dev/null; then
             echo "❌ No production rules found in grammar"
             exit 1
           fi
           echo "✅ Grammar file appears valid"
 
+      # Filenames corrected: these are GQL-DT-*, not GQLdt-*. The old list made
+      # this job fail on a spelling mismatch and report it as a MISSING SPEC.
       - name: Verify specification files
         run: |
+          missing=0
           for file in spec/GQL_Dependent_Types_Complete_Specification.md \
                       spec/normalization-types.md \
                       spec/GQLdt-Grammar.ebnf \
-                      spec/GQLdt-Lexical.md \
-                      spec/GQLdt-Railroad-Diagrams.md; do
+                      spec/GQL-DT-Lexical.md \
+                      spec/GQL-DT-Railroad-Diagrams.md; do
             if [ ! -f "$file" ]; then
               echo "❌ Missing required spec file: $file"
-              exit 1
+              missing=1
             fi
           done
+          [ "$missing" -eq 0 ] || exit 1
           echo "✅ All specification files present"
 
-      - name: Check for naming consistency
-        run: |
-          echo "Checking for naming inconsistencies..."
-          # Check STATE.scm and ECOSYSTEM.scm use gql-dt not gql-dt
-          if grep -i "gql-dt" STATE.scm ECOSYSTEM.scm 2>/dev/null; then
-            echo "❌ Found old naming (gql-dt instead of gql-dt)"
-            exit 1
-          fi
-          echo "✅ Naming is consistent"
+      # REMOVED: a "naming consistency" step that ran
+      #     grep -i "gql-dt" STATE.scm ECOSYSTEM.scm 2>/dev/null
+      #   -> echo "Found old naming (gql-dt instead of gql-dt)"
+      # It compared a string to itself, over two files that do not exist in this
+      # repo (2>/dev/null swallowed the error), so it could only ever pass.
+      # Deleted rather than repaired: there is no naming rule for it to enforce.
 
   documentation:
     name: Build Documentation

.github/workflows/scorecard.yml

@@ -9,11 +9,19 @@ on:
 
 permissions: read-all
 
+# Estate policy (standards/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc and the workflow
+# staleness check): OSSF Scorecard MUST NOT upload SARIF to GitHub Code Scanning unless
+# it runs for every PR head commit. This workflow runs on push-to-main and on a schedule,
+# NOT on pull_request — so Code Scanning would show findings that correspond to no PR
+# head commit, and PR checks would appear to carry security results they do not.
+#
+# Resolution: keep the scan, drop the Code Scanning upload. The SARIF is retained as a
+# build artifact instead, which is inspectable without polluting Code Scanning.
+
 jobs:
   analysis:
     runs-on: ubuntu-latest
     permissions:
-      security-events: write
       id-token: write
     steps:
       - uses: actions/checkout@8e8c483db84b4bee98b60c0593521ed34d9990e8 # v6.0.1
@@ -26,7 +34,10 @@ jobs:
           results_file: results.sarif
           results_format: sarif
 
-      - name: Upload results
-        uses: github/codeql-action/upload-sarif@cdefb33c0f6224e58673d9004f47f7cb3e328b89 # v3.31.8
+      # NOT github/codeql-action/upload-sarif — see the policy note above.
+      - name: Upload results as artifact
+        uses: actions/upload-artifact@26f96dfa697d77e81fd5907df203aa23a56210a8 # v4
         with:
-          sarif_file: results.sarif
+          name: scorecard-results
+          path: results.sarif
+          retention-days: 30

.machine_readable/6a2/AGENTIC.a2ml

@@ -19,7 +19,7 @@ can-create-files = true
 # - Never commit secrets or credentials
 # - Never use banned languages (TypeScript, Python, Go, etc.)
 # - Never place state files in repository root (must be in .machine_readable/)
-# - Never use AGPL license (use PMPL-1.0-or-later)
+# - Never use AGPL license. Code = MPL-2.0, documentation (.md/.adoc) = CC-BY-SA-4.0
 
 [maintenance-integrity]
 fail-closed = true

.machine_readable/6a2/META.a2ml

@@ -7,7 +7,7 @@ version = "1.0.0"
 last-updated = "2026-04-11"
 
 [project-info]
-license = "PMPL-1.0-or-later"
+license = "MPL-2.0"
 author = "Jonathan D.A. Jewell (hyperpolymath)"
 
 [architecture-decisions]

0-AI-MANIFEST.a2ml

@@ -9,8 +9,8 @@
     (name "GQL-DT")
     (full-name "Dependently-Typed Glyph Query Language")
     (version "0.2.0")
-    (repo "https://github.com/hyperpolymath/gql-dt")
-    (license "PMPL-1.0-or-later")
+    (repo "https://github.com/hyperpolymath/gnpl")
+    (license "MPL-2.0")
     (author "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>")
     (parent-project "lithoglyph")
     (monorepo-parent "nextgen-databases"))

ABI-FFI-README.md

@@ -374,7 +374,7 @@ When modifying the ABI/FFI:
 
 ## License
 
-PMPL-1.0-or-later
+CC-BY-SA-4.0
 
 ## See Also
 

Containerfile

@@ -9,7 +9,7 @@ FROM ubuntu:24.04
 LABEL org.opencontainers.image.title="GQLdt Development Environment"
 LABEL org.opencontainers.image.description="Lean 4 + Zig for dependently-typed Lith queries"
 LABEL org.opencontainers.image.authors="Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
-LABEL org.opencontainers.image.licenses="PMPL-1.0-or-later"
+LABEL org.opencontainers.image.licenses="MPL-2.0"
 
 # Install system dependencies
 RUN apt-get update && apt-get install -y \

GQL-DT-COMPLETION-2026-02-07.md

@@ -169,7 +169,7 @@ deno run --allow-net --allow-read cli/lsp-server.ts
   "description": "Language support for GQL-DT queries with dependent type checking",
   "version": "1.0.0",
   "publisher": "hyperpolymath",
-  "license": "PMPL-1.0-or-later",
+  "license": "MPL-2.0",
   "engines": { "vscode": "^1.80.0" }
 }
 ```
@@ -557,4 +557,4 @@ All standard tooling is built, tested, and functional:
 
 **Report Generated:** 2026-02-07
 **Author:** Claude Sonnet 4.5 (Hyperpolymath Standards)
-**License:** PMPL-1.0-or-later
+**License:** CC-BY-SA-4.0