From 4dc4c933fac7265d3c59961ad7942a9a44b511c2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 17:13:16 +0000 Subject: [PATCH 1/4] chore(proofs): clear unused-variable lint warnings _-prefix intentionally-unused binders across JtvTheorems/JtvOperational/JtvTypes/JtvSecurity/JtvExtended. lake build stays green (8 libs, 0 sorry/admit/axiom, now 0 warnings). https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- jtv_proofs/JtvExtended.lean | 2 +- jtv_proofs/JtvOperational.lean | 2 +- jtv_proofs/JtvSecurity.lean | 2 +- jtv_proofs/JtvTheorems.lean | 10 +++++----- jtv_proofs/JtvTypes.lean | 6 +++--- 5 files changed, 11 insertions(+), 11 deletions(-) diff --git a/jtv_proofs/JtvExtended.lean b/jtv_proofs/JtvExtended.lean index 0c24c65..806c470 100644 --- a/jtv_proofs/JtvExtended.lean +++ b/jtv_proofs/JtvExtended.lean @@ -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 diff --git a/jtv_proofs/JtvOperational.lean b/jtv_proofs/JtvOperational.lean index c8a2dab..44ae55a 100644 --- a/jtv_proofs/JtvOperational.lean +++ b/jtv_proofs/JtvOperational.lean @@ -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₂] diff --git a/jtv_proofs/JtvSecurity.lean b/jtv_proofs/JtvSecurity.lean index 99c7a85..efad548 100644 --- a/jtv_proofs/JtvSecurity.lean +++ b/jtv_proofs/JtvSecurity.lean @@ -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 diff --git a/jtv_proofs/JtvTheorems.lean b/jtv_proofs/JtvTheorems.lean index 47d0ced..4124f5d 100644 --- a/jtv_proofs/JtvTheorems.lean +++ b/jtv_proofs/JtvTheorems.lean @@ -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⟩ -- ============================================================================ diff --git a/jtv_proofs/JtvTypes.lean b/jtv_proofs/JtvTypes.lean index 89acded..577949e 100644 --- a/jtv_proofs/JtvTypes.lean +++ b/jtv_proofs/JtvTypes.lean @@ -429,10 +429,10 @@ 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 σ) /-- @@ -440,7 +440,7 @@ theorem type_preservation (Γ : TypeEnv) (e : DataExpr) (τ : JtvType) (σ : Sta 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 From e810de487967e38799b8f4a8d68a8b8818f098ad Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 17:13:16 +0000 Subject: [PATCH 2/4] chore(license): SPDX headers on 17 wiki files; add .github/CODEOWNERS Every wiki/*.md lacked the SPDX-License-Identifier the repo security policy mandates; prepend MPL-2.0 headers. Salvage CODEOWNERS (sole-maintainer review routing) from estate-standardization-20260607, corrected to the estate-wave .machine_readable/contractiles path. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .github/CODEOWNERS | 36 +++++++++++++++++++++++++++ wiki/Home.md | 5 ++++ wiki/compiler/Architecture.md | 5 ++++ wiki/internals/Purity-System.md | 5 ++++ wiki/internals/Security.md | 5 ++++ wiki/internals/Type-System.md | 5 ++++ wiki/language/Control-Language.md | 5 ++++ wiki/language/Data-Language.md | 5 ++++ wiki/language/Harvard-Architecture.md | 5 ++++ wiki/language/Number-Systems.md | 5 ++++ wiki/language/Reversible-Computing.md | 5 ++++ wiki/language/Syntax-Overview.md | 5 ++++ wiki/reference/Grammar.md | 5 ++++ wiki/stdlib/Overview.md | 5 ++++ wiki/tooling/CLI.md | 5 ++++ wiki/tooling/LSP.md | 5 ++++ wiki/tooling/Property-Testing.md | 5 ++++ wiki/tutorials/Getting-Started.md | 5 ++++ 18 files changed, 121 insertions(+) create mode 100644 .github/CODEOWNERS diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS new file mode 100644 index 0000000..bdd41cb --- /dev/null +++ b/.github/CODEOWNERS @@ -0,0 +1,36 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# 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 diff --git a/wiki/Home.md b/wiki/Home.md index fc080a3..5fac4a0 100644 --- a/wiki/Home.md +++ b/wiki/Home.md @@ -1,3 +1,8 @@ + + # Julia the Viper Wiki Welcome to the Julia the Viper documentation wiki. diff --git a/wiki/compiler/Architecture.md b/wiki/compiler/Architecture.md index b3e03b9..27c8571 100644 --- a/wiki/compiler/Architecture.md +++ b/wiki/compiler/Architecture.md @@ -1,3 +1,8 @@ + + # JtV Compiler Architecture The JtV compiler transforms source code into executable form while enforcing the Harvard Architecture guarantees. diff --git a/wiki/internals/Purity-System.md b/wiki/internals/Purity-System.md index 9dbb202..8ca414e 100644 --- a/wiki/internals/Purity-System.md +++ b/wiki/internals/Purity-System.md @@ -1,3 +1,8 @@ + + # JtV Purity System The purity system enforces the Harvard Architecture by tracking function purity at compile time. diff --git a/wiki/internals/Security.md b/wiki/internals/Security.md index 1997434..695086f 100644 --- a/wiki/internals/Security.md +++ b/wiki/internals/Security.md @@ -1,3 +1,8 @@ + + # JtV Security Model JtV provides **security by design** through its Harvard Architecture, making entire categories of vulnerabilities grammatically impossible. diff --git a/wiki/internals/Type-System.md b/wiki/internals/Type-System.md index 5b81ab4..39835ec 100644 --- a/wiki/internals/Type-System.md +++ b/wiki/internals/Type-System.md @@ -1,3 +1,8 @@ + + # JtV Type System The JtV type system provides static type checking with automatic inference and coercion for the 7 number systems. diff --git a/wiki/language/Control-Language.md b/wiki/language/Control-Language.md index 95be254..73e0f12 100644 --- a/wiki/language/Control-Language.md +++ b/wiki/language/Control-Language.md @@ -1,3 +1,8 @@ + + # Control Language The Control Language is JtV's **Turing-complete** sublanguage for imperative programming. diff --git a/wiki/language/Data-Language.md b/wiki/language/Data-Language.md index de00d78..85d74b5 100644 --- a/wiki/language/Data-Language.md +++ b/wiki/language/Data-Language.md @@ -1,3 +1,8 @@ + + # Data Language The Data Language is JtV's **decidable**, **total** sublanguage for pure computation. diff --git a/wiki/language/Harvard-Architecture.md b/wiki/language/Harvard-Architecture.md index 994233c..9416dba 100644 --- a/wiki/language/Harvard-Architecture.md +++ b/wiki/language/Harvard-Architecture.md @@ -1,3 +1,8 @@ + + # Harvard Architecture in JtV ## Overview diff --git a/wiki/language/Number-Systems.md b/wiki/language/Number-Systems.md index ac329d0..6fe43b9 100644 --- a/wiki/language/Number-Systems.md +++ b/wiki/language/Number-Systems.md @@ -1,3 +1,8 @@ + + # Number Systems JtV supports **7 number systems** with automatic type coercion and exact arithmetic where possible. diff --git a/wiki/language/Reversible-Computing.md b/wiki/language/Reversible-Computing.md index 0a966f2..9c83921 100644 --- a/wiki/language/Reversible-Computing.md +++ b/wiki/language/Reversible-Computing.md @@ -1,3 +1,8 @@ + + # Reversible Computing in JtV JtV v2 introduces **reversible computing** through `reverse` blocks, enabling quantum algorithm simulation and thermodynamically efficient computation. diff --git a/wiki/language/Syntax-Overview.md b/wiki/language/Syntax-Overview.md index a3a8025..6f077c9 100644 --- a/wiki/language/Syntax-Overview.md +++ b/wiki/language/Syntax-Overview.md @@ -1,3 +1,8 @@ + + # JtV Syntax Overview ## Basic Structure diff --git a/wiki/reference/Grammar.md b/wiki/reference/Grammar.md index adc2dcf..6834f74 100644 --- a/wiki/reference/Grammar.md +++ b/wiki/reference/Grammar.md @@ -1,3 +1,8 @@ + + # JtV Grammar Reference Complete EBNF grammar specification for Julia the Viper. diff --git a/wiki/stdlib/Overview.md b/wiki/stdlib/Overview.md index 0a19b3a..15877d8 100644 --- a/wiki/stdlib/Overview.md +++ b/wiki/stdlib/Overview.md @@ -1,3 +1,8 @@ + + # JtV Standard Library Overview The JtV standard library provides essential functions and types organized into modules. diff --git a/wiki/tooling/CLI.md b/wiki/tooling/CLI.md index 0946865..3033925 100644 --- a/wiki/tooling/CLI.md +++ b/wiki/tooling/CLI.md @@ -1,3 +1,8 @@ + + # JtV Command Line Interface The `jtv` CLI is the primary tool for working with Julia the Viper programs. diff --git a/wiki/tooling/LSP.md b/wiki/tooling/LSP.md index d45acaf..4ba4394 100644 --- a/wiki/tooling/LSP.md +++ b/wiki/tooling/LSP.md @@ -1,3 +1,8 @@ + + # JtV Language Server Protocol The JtV LSP provides IDE integration for editors supporting the Language Server Protocol. diff --git a/wiki/tooling/Property-Testing.md b/wiki/tooling/Property-Testing.md index c1b07af..771e9bd 100644 --- a/wiki/tooling/Property-Testing.md +++ b/wiki/tooling/Property-Testing.md @@ -1,3 +1,8 @@ + + # 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. diff --git a/wiki/tutorials/Getting-Started.md b/wiki/tutorials/Getting-Started.md index e6568f6..0d175af 100644 --- a/wiki/tutorials/Getting-Started.md +++ b/wiki/tutorials/Getting-Started.md @@ -1,3 +1,8 @@ + + # Getting Started with Julia the Viper Welcome to Julia the Viper (JtV), a security-focused programming language that makes code injection **grammatically impossible**. From 9370b17156d97ff3fdf2013525a641fff6cb3a98 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 17:13:16 +0000 Subject: [PATCH 3/4] ci(codeql): weekly -> monthly scan cron Cut shared-Actions-pool noise (standards#288). Folds in the sole change carried by the codeql-cron-monthly stray branch. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .github/workflows/codeql.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 94ba8ff..f485020 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -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 From a1ae47faf1edfbcf8a6ac672db47fac8b4cff1c3 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 15 Jun 2026 17:13:16 +0000 Subject: [PATCH 4/4] docs: ADR-0007 graded-comonad note; STATE refresh; flag PMPL/MPL discrepancy (gap-006) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ADR-0007 gains the graded-comonad / tropical-grade characterization (cross-links echo-types' establishment track) as the conceptual basis for the v2 (c) bridge. STATE.a2ml refreshed to 2026-06-15; gap-006 records that 8 files carry the non-SPDX PMPL-1.0 identifier while the rest of the repo + estate standard use MPL-2.0 — logged for a governance decision, NOT auto-changed. https://claude.ai/code/session_01BJmfoz1ZS1Pejy9LLMY742 --- .machine_readable/6a2/STATE.a2ml | 12 +++++---- ...nly-mandate-and-reversibility-tiering.adoc | 27 +++++++++++++++++++ 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 54a2b30..c5530b3 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -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] diff --git a/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc b/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc index 57fad1c..6626f23 100644 --- a/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc +++ b/docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc @@ -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