hyperpolymath · hyperpolymath · Jun 15, 2026 · Jun 15, 2026 · Jun 15, 2026 · Jun 15, 2026
@@ -0,0 +1,36 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# CODEOWNERS — code review assignments for GitHub.
+# See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners
+
+# Default: sole maintainer for all files
+* @hyperpolymath
+
+# Security-sensitive paths
+SECURITY.md @hyperpolymath
+.github/ @hyperpolymath
+.github/workflows/ @hyperpolymath
+.machine_readable/ @hyperpolymath
+
+# License files
+LICENSE @hyperpolymath
+LICENSES/ @hyperpolymath
+
+# Governance & documentation
+README* @hyperpolymath
+CONTRIBUTING* @hyperpolymath
+CODE_OF_CONDUCT* @hyperpolymath
+GOVERNANCE* @hyperpolymath
+MAINTAINERS* @hyperpolymath
+CHANGELOG* @hyperpolymath
+ROADMAP* @hyperpolymath
+
+# Build & CI (estate-wave: contractiles live under .machine_readable/)
+.machine_readable/contractiles/ @hyperpolymath
+Justfile @hyperpolymath
+*.sh @hyperpolymath
+
+# Formal proofs & verification (high-assurance)
+jtv_proofs/ @hyperpolymath
+verification/ @hyperpolymath
@@ -7,7 +7,7 @@ on:
   pull_request:
     branches: [main, master]
   schedule:
-    - cron: '0 6 * * 1'
+    - cron: '0 6 1 * *'   # monthly, 1st at 06:00 UTC (cut noise vs weekly; standards#288)
 
 # Estate guardrail: cancel superseded runs so re-pushes / rebased PR
 # updates do not pile up queued runs against the shared account-wide

@@ -5,9 +5,9 @@
 [metadata]
 project = "julia-the-viper"
 version = "0.0.1"
-last-updated = "2026-06-13"
+last-updated = "2026-06-15"
 status = "active"
-session = "2026-06-13 — PR #26 (Lean repair + Echo as structural type-system gate + root-cause Rust-CI fix) and PR #27 (de-vacuation of 8 True-typed believeme theorems) merged; ADR-0007 records the addition-only mandate + Echo reversibility tiering; governance-hardening + number-system-semantics + v2 (c) bridge queued"
+session = "2026-06-15 — bookkeeping/tidying consolidation: lake build green (8 libs, 0 sorry/admit/axiom, 0 vacuity, 0 lint warnings); 4 stray branches resolved (2 stale-merged deleted + codeql weekly->monthly cron folded + estate-standardization salvaged: CODEOWNERS + 17 wiki SPDX headers); ADR-0007 gains the graded-comonad/tropical-grade characterization note; PMPL-1.0 vs MPL-2.0 header discrepancy flagged for governance decision (gap-006); number-system-semantics + v2 (c) bridge remain queued"
 
 [project-context]
 name = "Julia The Viper"
@@ -50,7 +50,8 @@ issues = [
   { id = "gap-002", description = "typing_coercion in JtvTypes.lean weaker than docstring — proves existence not coercion to target type", severity = "low", status = "known", follow-up = "ADR needed" },
   { id = "gap-003", description = "Coprocessor implementation gated on PataCL Phase 1", severity = "medium", status = "external-dependency" },
   { id = "gap-004", description = "Reversibility round-trip not guaranteed end-to-end at integration level", severity = "medium", status = "known" },
-  { id = "gap-005", description = "Semantic model is Int-only: the 7 number systems are typed but stated-unproven at the value level; type_preservation mechanised only for τ=int (see ADR-0007 D6 + PROOF-CAPABILITY-MATRIX.adoc)", severity = "medium", status = "known", follow-up = "number-system-semantics work" }
+  { id = "gap-005", description = "Semantic model is Int-only: the 7 number systems are typed but stated-unproven at the value level; type_preservation mechanised only for τ=int (see ADR-0007 D6 + PROOF-CAPABILITY-MATRIX.adoc)", severity = "medium", status = "known", follow-up = "number-system-semantics work" },
+  { id = "gap-006", description = "License-identifier discrepancy: 8 files (codeql.yml, scorecard.yml, language-policy.yml, README.adoc, PALIMPSEST.adoc, playground/README.adoc, playground/PALIMPSEST.adoc, playground/jtv/README.adoc) carry SPDX-License-Identifier: PMPL-1.0, not an SPDX-recognised identifier; ADR-0007 + spec + 6a2 + new governance/wiki files use MPL-2.0 (PMPL noted only as aspirational). estate standard (absolute-zero) is MPL-2.0-only with PMPL-1.0 -> MPL-2.0. Needs governance decision: normalise to MPL-2.0, or formally keep/adopt PMPL via PALIMPSEST.adoc.", severity = "medium", status = "flagged", follow-up = "user governance decision" }
 ]
 
 [critical-next-actions]
@@ -64,7 +65,7 @@ actions = [
 ]
 
 [maintenance-status]
-last-run-utc = "2026-06-02T00:00:00Z"
+last-run-utc = "2026-06-15T00:00:00Z"
 last-result = "pass"  # unknown | pass | warn | fail
 
 [session-history]
@@ -80,7 +81,8 @@ sessions = [
   { date = "2026-06-02", subject = "Build-truth: patacl-core path dep removed from workspace; [features] patacl = [] pure code feature; proof-regression.yml startup failure fixed; Lean 4 all 5 libs compile; Idris2 Types.idr compiles; CI governance/language-policy/deno-lint fixes; documentation refresh" },
   { date = "2026-06-13", subject = "PR #26 merged: Lean suite repaired (JtvEcho.neg_injective; orphan JtvExtended wired in → 8 libs); Echo a structural type-system gate over BOTH reverse{} and reversible{}->tok (checked first, before type inference); fixed pre-existing failing reverse-block echo test; root-cause Rust-CI revival (rust-ci/coverage hashFiles-in-job-if startup failure since ~05-27); clippy lint cleared; workflow pins+timeouts; *.jtv/*.pata eol=lf" },
   { date = "2026-06-13", subject = "PR #27 merged: de-vacuated 8 True-typed believeme theorems (string_not_executable, confluence, no_vulnerable_constructs, no_reverse_joinpoints, dataExpr_no_control, data_evaluation_secure, control_data_noninterference, rev_composition) into real compiled statements; NO-VACUITY + Int-only-scope recorded in capability matrix" },
-  { date = "2026-06-13", subject = "ADR-0007: addition-only mandate (absolute; ×/÷ generated, not primitive); subtraction = reverse addition (not 2s-complement/not primitive); Harvard-in-von-Neumann AOLD insertability; shortest-path-to-equality + Echo lineage + cross-system routing; additive-algebra → reversibility-tier (group→Safe / cancellative→Neutral / idempotent→Breaking; Echo's own join is idempotent)" }
+  { date = "2026-06-13", subject = "ADR-0007: addition-only mandate (absolute; ×/÷ generated, not primitive); subtraction = reverse addition (not 2s-complement/not primitive); Harvard-in-von-Neumann AOLD insertability; shortest-path-to-equality + Echo lineage + cross-system routing; additive-algebra → reversibility-tier (group→Safe / cancellative→Neutral / idempotent→Breaking; Echo's own join is idempotent)" },
+  { date = "2026-06-15", subject = "Bookkeeping/tidying consolidation: confirmed lake build green (8 libs); cleared all Lean unused-variable lint warnings (_-prefix); resolved 4 stray remote branches (deleted 2 stale-merged changelog/tech-debt whose content is already on main; folded codeql weekly->monthly cron; salvaged CODEOWNERS + 17 wiki SPDX headers from estate-standardization-20260607, dropped its superseded pre-repair Lean drafts + old contractiles); ADR-0007 graded-comonad/tropical-grade characterization note; flagged PMPL-1.0 vs MPL-2.0 discrepancy (gap-006)" }
 ]
 
 [design-artefact-locations]

@@ -141,6 +141,33 @@ semirings, lattices). In such systems the D5 ladder is *forced*: Safe
 is impossible, so one must keep a residue (Neutral) or accept Breaking.
 ====
 
+=== Theoretical characterization (note for continuity): Echo is a graded comonad with a tropical grade
+
+Recording the characterization that situates the D1–D6 tiering in
+type-theoretic terms, so later work can build on it directly:
+
+* *Echo is a graded comonad of structured loss.* The grade is the
+  reversibility tier `{Safe ⊑ Neutral ⊑ Breaking}`; `extract` forgets the
+  retained lineage and `duplicate` splits it, and grades compose by the
+  lattice join. This is precisely the object the companion `echo-types`
+  development formalises and pins on its establishment track (a
+  *characterised graded comonad of structured loss* — coeffect /
+  quantitative-lineage, explicitly not the linear/dependent judgmental
+  ladder).
+* *The grade is a tropical (idempotent, min-plus-style) modality.* Join
+  is idempotent (the D6 self-reference NOTE), so loss composition takes
+  the worst tier and admits no inverse — which is exactly why `Breaking`
+  is one-way and why a `Neutral` reverse needs a retained residue (D5).
+* *Operational reading.* JtV's reversibility tiering (D5/D6) is the
+  operational face of that graded comonad: the grade attached to a
+  computation is the best reversal tier still attainable, and Echo is the
+  bookkeeping of that grade across number-system hops (D4).
+
+This is a characterisation, not a new JtV obligation: JtV does **not**
+re-mechanise the graded-comonad laws — those are proved in `echo-types`
+(its Pillar B is complete). JtV consumes the result as the conceptual
+basis for the v2 `(c)` Neutral bridge and the number-system → tier map.
+
 == Consequences
 
 . *Number-system semantics work (next-but-one priority).* The Lean model

@@ -238,7 +238,7 @@ def dependsOn (e : DataExpr) (x : String) : Prop :=
   The only dependencies are through free variables.
 -/
 theorem no_hidden_deps (e : DataExpr) (x : String) (σ₁ σ₂ : State)
-    (hx : x ∉ e.freeVars)
+    (_hx : x ∉ e.freeVars)
     (heq : ∀ y ∈ e.freeVars, σ₁ y = σ₂ y) :
     evalDataExpr e σ₁ = evalDataExpr e σ₂ := by
   apply free_vars_sufficient

@@ -160,7 +160,7 @@ theorem bigstep_denotational_equiv (e : DataExpr) (σ : State) (n : Int) :
   constructor
   · intro h
     induction h with
-    | lit n' σ' => simp [evalDataExpr]
+    | lit n' _σ' => simp [evalDataExpr]
     | var x σ' => simp [evalDataExpr]
     | add e₁ e₂ σ' n₁ n₂ _ _ ih₁ ih₂ =>
       simp [evalDataExpr, ih₁, ih₂]

@@ -313,7 +313,7 @@ theorem aold_complete :
 -/
 
 /-- Model of eval() vulnerability in traditional languages -/
-def evalVulnerability (userInput : String) : Prop :=
+def evalVulnerability (_userInput : String) : Prop :=
   -- In vulnerable languages, any string can become code
   -- This is NOT possible in JtV
   True

@@ -44,8 +44,8 @@ theorem expr_totality (e : Expr) (σ : State) : ∃ (n : Int), evalExpr e σ = n
     obtain ⟨n, h⟩ := term_totality t σ
     exact ⟨n, h⟩
   | add t₁ t₂ =>
-    obtain ⟨n₁, _⟩ := term_totality t₁ σ
-    obtain ⟨n₂, _⟩ := term_totality t₂ σ
+    obtain ⟨_n₁, _⟩ := term_totality t₁ σ
+    obtain ⟨_n₂, _⟩ := term_totality t₂ σ
     exact ⟨evalTerm t₁ σ + evalTerm t₂ σ, rfl⟩
 
 /--
@@ -60,11 +60,11 @@ theorem dataExpr_totality (e : DataExpr) (σ : State) : ∃ (n : Int), evalDataE
   | lit n => exact ⟨n, rfl⟩
   | var x => exact ⟨σ x, rfl⟩
   | add e₁ e₂ ih₁ ih₂ =>
-    obtain ⟨n₁, _⟩ := ih₁
-    obtain ⟨n₂, _⟩ := ih₂
+    obtain ⟨_n₁, _⟩ := ih₁
+    obtain ⟨_n₂, _⟩ := ih₂
     exact ⟨evalDataExpr e₁ σ + evalDataExpr e₂ σ, rfl⟩
   | neg e ih =>
-    obtain ⟨n, _⟩ := ih
+    obtain ⟨_n, _⟩ := ih
     exact ⟨-(evalDataExpr e σ), rfl⟩
 
 -- ============================================================================

@@ -429,18 +429,18 @@ inductive TypedValue : Int → JtvType → Prop where
   If Γ ⊢ e : τ and e evaluates to v, then v has type τ.
 -/
 theorem type_preservation (Γ : TypeEnv) (e : DataExpr) (τ : JtvType) (σ : State)
-    (h : DataTyping Γ e τ) :
+    (_h : DataTyping Γ e τ) :
     -- For integer types, the result is an integer
     τ = JtvType.int → TypedValue (evalDataExpr e σ) JtvType.int := by
-  intro hτ
+  intro _hτ
   exact TypedValue.int (evalDataExpr e σ)
 
 /--
   **Theorem (Progress for Typed Terms)**:
   If Γ ⊢ e : τ, then either e is a value or e can step.
 -/
 theorem typed_progress (Γ : TypeEnv) (e : DataExpr) (τ : JtvType)
-    (h : DataTyping Γ e τ) :
+    (_h : DataTyping Γ e τ) :
     e.isValue = true ∨ ∃ e', DataStep ⟨e, State.empty⟩ ⟨e', State.empty⟩ := by
   exact data_progress e State.empty
 

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # Julia the Viper Wiki
 
 Welcome to the Julia the Viper documentation wiki.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Compiler Architecture
 
 The JtV compiler transforms source code into executable form while enforcing the Harvard Architecture guarantees.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Purity System
 
 The purity system enforces the Harvard Architecture by tracking function purity at compile time.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Security Model
 
 JtV provides **security by design** through its Harvard Architecture, making entire categories of vulnerabilities grammatically impossible.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Type System
 
 The JtV type system provides static type checking with automatic inference and coercion for the 7 number systems.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # Control Language
 
 The Control Language is JtV's **Turing-complete** sublanguage for imperative programming.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # Data Language
 
 The Data Language is JtV's **decidable**, **total** sublanguage for pure computation.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # Harvard Architecture in JtV
 
 ## Overview

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # Number Systems
 
 JtV supports **7 number systems** with automatic type coercion and exact arithmetic where possible.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # Reversible Computing in JtV
 
 JtV v2 introduces **reversible computing** through `reverse` blocks, enabling quantum algorithm simulation and thermodynamically efficient computation.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Syntax Overview
 
 ## Basic Structure

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Grammar Reference
 
 Complete EBNF grammar specification for Julia the Viper.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Standard Library Overview
 
 The JtV standard library provides essential functions and types organized into modules.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Command Line Interface
 
 The `jtv` CLI is the primary tool for working with Julia the Viper programs.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # JtV Language Server Protocol
 
 The JtV LSP provides IDE integration for editors supporting the Language Server Protocol.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # Property-Based Testing in JtV
 
 JtV supports property-based testing inspired by tools like QuickCheck, Hypothesis, and **Echidna** (smart contract fuzzer). Instead of writing individual test cases, you specify properties that should always hold.

@@ -1,3 +1,8 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+-->
+
 # Getting Started with Julia the Viper
 
 Welcome to Julia the Viper (JtV), a security-focused programming language that makes code injection **grammatically impossible**.