hyperpolymath · hyperpolymath · Jun 18, 2026 · Jun 18, 2026
@@ -5,9 +5,9 @@
 [metadata]
 project = "julia-the-viper"
 version = "0.0.1"
-last-updated = "2026-06-15"
+last-updated = "2026-06-18"
 status = "active"
-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 flagged for UI deletion — git push --delete returned 403 — + 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); v2 (c) Neutral reversal bridge LANDED (Lean + Rust, green); number-system-semantics (gap-005) remains the next rung"
+session = "2026-06-18 — Echo arc completed + number systems stratified. (b) Echo+Epistemic first-class DONE (proof side, ADR-0009): JtvEcho.lean SECTION 5 = Epistemic lattice + Echo×Epistemic product FunctionEffect lattice + comm/assoc/idem composition laws (matching the already-merged echo.rs/epistemic.rs/effect.rs). Number systems STRATIFIED (ADR-0007 D6 realized as ADR-0010): JtvEcho.lean SECTION 6 3-level NumAlgebra tower 1:1 with the Echo lattice (hex/binary=ℤ-encodings collapse to int's tier; float=approxGroup→Neutral); echo.rs carrier-aware classification (CarrierEnv; reversible += graded shape⊔carrier; default-carrier=Int sound) + effect.rs param-seeded env; number.rs runtime-value bridge Value::reversal_echo. PR #44 merged (rebase); bridge+ADR-0010 PR next. lake + cargo green (124 lib tests, 0 sorry/unwrap). NEXT rung: float-LOCALS soundness slice (thread typechecker inferred types into CarrierEnv) + value-level semantics (gap-005)"
 
 [project-context]
 name = "Julia The Viper"
@@ -50,22 +50,22 @@ 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). PARTIAL 2026-06-18 (ADR-0010): per-system additive-algebra → Echo-tier CLASSIFICATION now landed at proof/type/value level (JtvEcho SECTION 6, echo.rs carrier_echo, number.rs Value::reversal_echo); the remaining open half is the type_preservation/round-trip SEMANTICS beyond τ=int", severity = "medium", status = "known", follow-up = "value-level semantics for τ≠int; float-locals CarrierEnv inference slice" },
   { id = "gap-006", description = "RESOLVED 2026-06-15: license decision = MPL-2.0 (code) + CC-BY-SA-4.0 (docs), full per-file. 75 doc headers -> CC-BY-SA-4.0; code stragglers (3 PMPL-1.0 workflows, MPL-2.0-or-later, PLMP/GPL typos, and a deliberate MIT-OR-GPL-3.0-or-later-OR-Palimpsest tri-license on formatter/repl/rsr_check) -> MPL-2.0; PALIMPSEST.adoc (both copies) retired; LICENSING.md rewritten; PMPL badges replaced. Follow-ups: populate LICENSES/ with canonical MPL-2.0 + CC-BY-SA-4.0 texts; add SPDX headers to ~49 header-less docs.", severity = "low", status = "resolved", follow-up = "LICENSES/ texts + header-less docs" }
 ]
 
 [critical-next-actions]
 actions = [
   "Governance hardening (branch claude/jtv-governance-hardening): pin governance-reusable@main → SHA (consistent with sibling standards reusables); add secret-scanner.yml wrapper (standards reusable exists at 524523c); add 'actions' language to codeql.yml; harden proof-regression download-then-run; NOTE the reusable-call-job missing-timeout Hypatia findings are false-positives (timeout-minutes is invalid on reusable-call jobs)",
-  "Number-system semantics (ADR-0007 D6): value model for the 7 systems + per-system additive-algebra → Echo-tier classification; keep addition-only (×/÷ generated, not primitive); lift type_preservation beyond τ=int",
+  "Number-system stratification (ADR-0007 D6 / ADR-0010) — LANDED 2026-06-18: per-system additive-algebra → Echo-tier classification at proof level (JtvEcho.lean SECTION 6), type level (echo.rs carrier_echo + CarrierEnv carrier-aware += grading, effect.rs param-seeded env) and value level (number.rs Value::reversal_echo). STILL OPEN: (a) thread typechecker INFERRED types into CarrierEnv so float LOCALS grade Neutral — param-only today, so a reverse{} over a float local is wrongly Safe-admitted (soundness slice, NEXT); (b) lift type_preservation semantics beyond τ=int (gap-005); keep addition-only (×/÷ generated)",
   "v2 (c) token/residue neutral-reversal bridge — LANDED 2026-06-15 (ADR-0007 D5 Neutral tier): JtvEcho admissibleWithResidue + blockEcho_admissibleWithResidue; JtvTheorems execBackwardWithToken + rev_forward_backward_with_token + rev_backward_naive_fails_self_ref; echo.rs self-ref Breaking->Neutral; typechecker.rs check_echo_admissible_with_residue (token unlocks Neutral); reversible.rs RecordedOp::Snapshot residue. NEXT: (b) Echo as a first-class function effect",
-  "Echo as first-class function effect ('(b)') — after (c) stabilises",
+  "Echo as first-class function effect ('(b)') — LANDED 2026-06-18 (ADR-0009): echo.rs function_echo + epistemic.rs function_epistemic + effect.rs FunctionEffect row + resolved_effects call-graph fixpoint; JtvEcho.lean SECTION 5 mechanises the Echo×Epistemic product lattice + comm/assoc/idem composition laws",
   "Verification bridge: correlation tests between Lean semantics and Rust interpreter",
   "PataCL Phase 1 → unblocks JtV coproc implementation Phase 2"
 ]
 
 [maintenance-status]
-last-run-utc = "2026-06-15T00:00:00Z"
+last-run-utc = "2026-06-18T00:00:00Z"
 last-result = "pass"  # unknown | pass | warn | fail
 
 [session-history]
@@ -86,14 +86,16 @@ sessions = [
   { date = "2026-06-15", subject = "Security-hygiene clean (post-#33): triaged the Hypatia 67-finding report — informational (--exit-zero, gate passed), none originating from #33. Added CodeQL actions language; DELETED the frozen playground/experiments/_attic archive (17 files incl. stray npm package.json + a Julia demo), clearing both criticals + several highs at the source, with all dangling refs cleaned (deno.json excludes, bot_directives/hypatia.a2ml, .hypatia-ignore, playground README/Justfile); documented rsr_check.rs unsafe_block as a verified false-positive (Hypatia matched the RSR checker's own detection string). Deferred to a deliberate governance-hardening pass: secret-scanner.yml creation, scorecard job-perms, curl|sh install hardening." },
   { date = "2026-06-15", subject = "v2 (c) Neutral reversal bridge LANDED (Lean + Rust). Lean: JtvTheorems execBackwardWithToken + rev_forward_backward_with_token (full-state Bennett recovery, unconditional even for self-referential x += x) + rev_backward_naive_fails_self_ref (token necessary); JtvEcho admissibleWithResidue + blockEcho_admissibleWithResidue + admissible_implies_admissibleWithResidue + neutral_residue_only. Rust: echo.rs reclassifies self-reference Breaking->Neutral (token-recoverable, not erasure; Breaking reserved for future non-group/tropical systems per D6); typechecker.rs splits the Echo gate — reversible{}->tok uses check_echo_admissible_with_residue (admits Neutral; tokenless + reverse{} stay Safe-only); reversible.rs RecordedOp::Snapshot records/restores the residue. lake build + cargo test (99 lib + integration) + clippy -D warnings all green." },
   { date = "2026-06-17", subject = "License + hardening + ADR-0008. License (gap-006 RESOLVED, PR #36 merged): full per-file SPDX = MPL-2.0 (code) + CC-BY-SA-4.0 (docs); 190 MPL + 77 CC-BY-SA headers; PALIMPSEST.adoc retired; LICENSING.md rewritten; stray MIT/GPL/PMPL/or-later normalised. (PR #34 security clean + #35 v2-c bridge also merged earlier.) Workflow hardening (PR #37 merged): curl|sh installers (proof-regression elan, setup.sh just) -> download-then-run; rsr_check.rs unsafe_block self-trip cleared. Deferred (need hyperpolymath/standards reusable, out of session MCP scope): secret-scanner.yml, scorecard.yml job-perms. ADR-0008 (this commit): neg -> reverse-only; purist/adulterated dialect via feature-gated sugar + discouragement lint + purity certificate (resolves ADR-0007 D2); implementation is follow-on." },
-  { date = "2026-06-18", subject = "neg-dialect impl slice 1 + ADR-0009. PR #39 merged: jtv-core dialect.rs purity certificate (ADR-0008 D4) -- read-only AST scan stamping a program purist-jtv vs adulterated-jtv by counting expression-level neg sugar; reverse-block subtraction stays purist; 5 tests; cleared a self-introduced Hypatia unwrap_dangerous_default critical via Option::iter().sum(). ADR-0009 (this commit): Echo + Epistemic as first-class GRADED FUNCTION EFFECTS -- Echo grade {Safe<=Neutral<=Breaking} carried in the arrow, composing by the existing join; Epistemic = knowledge/observability axis {Opaque<=Partial<=Transparent} as a parallel graded effect (dual to Echo: loss vs revelation); product-lattice effect row; orthogonal to Purity + the dialect certificate. Implementation slice-wise (Echo-effect first). Still parked: (b) impl, number-system semantics, license wave-2, standards-blocked hardening (secret-scanner/scorecard)." }
+  { date = "2026-06-18", subject = "neg-dialect impl slice 1 + ADR-0009. PR #39 merged: jtv-core dialect.rs purity certificate (ADR-0008 D4) -- read-only AST scan stamping a program purist-jtv vs adulterated-jtv by counting expression-level neg sugar; reverse-block subtraction stays purist; 5 tests; cleared a self-introduced Hypatia unwrap_dangerous_default critical via Option::iter().sum(). ADR-0009 (this commit): Echo + Epistemic as first-class GRADED FUNCTION EFFECTS -- Echo grade {Safe<=Neutral<=Breaking} carried in the arrow, composing by the existing join; Epistemic = knowledge/observability axis {Opaque<=Partial<=Transparent} as a parallel graded effect (dual to Echo: loss vs revelation); product-lattice effect row; orthogonal to Purity + the dialect certificate. Implementation slice-wise (Echo-effect first). Still parked: (b) impl, number-system semantics, license wave-2, standards-blocked hardening (secret-scanner/scorecard)." },
+  { date = "2026-06-18", subject = "Echo arc completed + number-system stratification (PR #44 merged via rebase → main: SECTION 5+6 + carrier-aware echo; then bridge+ADR-0010 PR). (b) Echo+Epistemic first-class DONE on the proof side: JtvEcho.lean SECTION 5 = Epistemic lattice (hidden/bounded/full) + Echo×Epistemic product FunctionEffect lattice + comm/assoc/idem composition laws (mirrors the already-merged echo.rs/epistemic.rs/effect.rs). Number systems STRATIFIED (ADR-0007 D6 realized as ADR-0010): JtvEcho.lean SECTION 6 = 3-level NumAlgebra tower (abelianGroup/approxGroup/nonGroup) 1:1 with the Echo lattice; theorems hex_binary_collapse (hex/binary are ℤ-encodings, share int's tier) / exact_groups_safe / float_not_safe (IEEE-754 non-associative → approxGroup → Neutral) / no_current_system_breaks / reversal_tier_by_algebra. echo.rs made carrier-aware: NumAlgebra/additive_algebra/carrier_echo + CarrierEnv threaded through classify_*_in_env/function_echo_in_env; a reversible += is graded shape⊔carrier (float += → Neutral); shape-only wrappers preserve prior behaviour (empty env ⇒ Int=Safe); default-carrier=Int is sound (literals default to int). effect.rs own_effect seeds the env from param annotations. number.rs runtime-value bridge Value::number_system + Value::reversal_echo (delegates to carrier_echo — single source of truth). ADR-0010 reconciles with ADR-0007 D6 (float is approxGroup not D6-cancellative; D6's cancellative/idempotent Neutral/Breaking routes anticipated-but-uninhabited). lake + cargo fmt/clippy/test green (124 lib tests), 0 sorry/admit/axiom, no unwrap/unwrap_or. OPEN: float-LOCALS soundness slice (locals carry no annotation → thread typechecker inferred types into CarrierEnv, else a reverse{} over a float local is wrongly Safe-admitted); value-level type_preservation beyond τ=int (gap-005)." }
 ]
 
 [design-artefact-locations]
 coproc-adrs = "docs/design-decisions/0001-0006-*.adoc"
 addition-only-mandate-adr = "docs/design-decisions/0007-addition-only-mandate-and-reversibility-tiering.adoc"
 neg-dialect-adr = "docs/design-decisions/0008-neg-reverse-only-and-purist-dialect.adoc"
 echo-epistemic-effects-adr = "docs/design-decisions/0009-echo-epistemic-first-class-function-effects.adoc"
+number-system-stratification-adr = "docs/design-decisions/0010-number-system-stratification.adoc"
 proof-capability-matrix = "verification/PROOF-CAPABILITY-MATRIX.adoc"
 coproc-trajectories = ".machine_readable/COPROC-TRAJECTORIES.a2ml"
 v2-reversibility-design = "docs/language/DESIGN-JTV-V2-REVERSIBILITY.md"

@@ -1,5 +1,6 @@
 // Number system implementation supporting 7 types
-use crate::ast::Number;
+use crate::ast::{BasicType, Number};
+use crate::echo::{carrier_echo, Echo};
 use crate::error::{JtvError, Result};
 use num_complex::Complex64;
 use num_rational::Ratio;
@@ -26,6 +27,50 @@ pub enum Value {
     Unit,
 }
 
+// ============================================================================
+// NUMBER-SYSTEM STRATIFICATION — runtime-value bridge to Echo (ADR-0010)
+// ============================================================================
+// The runtime-value counterpart of the type-level `echo::carrier_echo`
+// (`BasicType -> Echo`) and the Lean `JtvEcho.lean` SECTION 6 stratification:
+// a runtime `Value`'s reversal tier is forced by the additive algebra of its
+// number system. The algebra -> tier map is NOT duplicated here — it is taken
+// from `echo::carrier_echo`, so there is a single source of truth.
+
+impl Value {
+    /// The number system this runtime value belongs to, or `None` for the
+    /// non-numeric carriers (bool / string / list / tuple / token / unit) —
+    /// which have no additive algebra and so cannot be `+=` targets.
+    pub fn number_system(&self) -> Option<BasicType> {
+        Some(match self {
+            Value::Int(_) => BasicType::Int,
+            Value::Float(_) => BasicType::Float,
+            Value::Rational(_) => BasicType::Rational,
+            Value::Complex(_) => BasicType::Complex,
+            Value::Hex(_) => BasicType::Hex,
+            Value::Binary(_) => BasicType::Binary,
+            Value::Symbolic(_) => BasicType::Symbolic,
+            Value::Bool(_)
+            | Value::String(_)
+            | Value::List(_)
+            | Value::Tuple(_)
+            | Value::ReversalToken(_)
+            | Value::Unit => return None,
+        })
+    }
+
+    /// The Echo reversal tier forced by this value's additive algebra — the
+    /// runtime-value counterpart of `echo::carrier_echo` and `JtvEcho.lean`
+    /// SECTION 6 (`abelianGroup -> Safe`, `approxGroup -> Neutral`,
+    /// `nonGroup -> Breaking`). A non-numeric value induces no additive-reversal
+    /// obligation, hence `Safe`.
+    pub fn reversal_echo(&self) -> Echo {
+        match self.number_system() {
+            Some(ty) => carrier_echo(&ty),
+            None => Echo::Safe,
+        }
+    }
+}
+
 impl Value {
     // Addition operation (the only arithmetic operation in Data Language)
     pub fn add(&self, other: &Value) -> Result<Value> {
@@ -338,4 +383,34 @@ mod tests {
         let result = a.add(&b).unwrap();
         assert!(matches!(result, Value::Float(_)));
     }
+
+    #[test]
+    fn value_number_system_maps_carriers() {
+        assert_eq!(Value::Int(0).number_system(), Some(BasicType::Int));
+        assert_eq!(Value::Float(0.0).number_system(), Some(BasicType::Float));
+        assert_eq!(Value::Hex(0).number_system(), Some(BasicType::Hex));
+        assert_eq!(Value::Binary(0).number_system(), Some(BasicType::Binary));
+        assert_eq!(
+            Value::Symbolic("x".to_string()).number_system(),
+            Some(BasicType::Symbolic)
+        );
+        // Non-numeric carriers have no additive algebra.
+        assert_eq!(Value::Bool(true).number_system(), None);
+        assert_eq!(Value::Unit.number_system(), None);
+        assert_eq!(Value::ReversalToken(0).number_system(), None);
+    }
+
+    #[test]
+    fn value_reversal_echo_mirrors_section6() {
+        // Exact abelian groups -> Safe (incl. the ℤ-encodings hex/binary).
+        assert_eq!(Value::Int(0).reversal_echo(), Echo::Safe);
+        assert_eq!(Value::Hex(0).reversal_echo(), Echo::Safe);
+        assert_eq!(Value::Binary(0).reversal_echo(), Echo::Safe);
+        assert_eq!(Value::Symbolic("x".to_string()).reversal_echo(), Echo::Safe);
+        // Float -> Neutral (non-associative, lossy reverse-add).
+        assert_eq!(Value::Float(1.5).reversal_echo(), Echo::Neutral);
+        // Non-numeric -> Safe (no additive-reversal obligation).
+        assert_eq!(Value::Bool(true).reversal_echo(), Echo::Safe);
+        assert_eq!(Value::Unit.reversal_echo(), Echo::Safe);
+    }
 }