hyperpolymath · hyperpolymath · Jun 21, 2026 · Jun 21, 2026
@@ -5,7 +5,7 @@
 [metadata]
 project = "jtv"
 version = "0.0.1"
-last-updated = "2026-06-18"
+last-updated = "2026-06-21"
 status = "active"
 session = "2026-06-18 — Surface Echo grades (ADR-0009 D1) + repo rename julia-the-viper→jtv. SURFACE ECHO: @echo(Safe|Neutral|Breaking) annotation on functions (grammar echo_marker + parser loop, order-independent with @pure); FunctionDecl.echo_annotation — the Echo enum moved ast.rs with an echo.rs `pub use` re-export to break the ast↔echo cycle; upper-bound check typechecker.rs check_echo_annotations (inferred ⊑ annotated, against the carrier-aware call-graph-composed effect.rs resolved_effects); pretty.rs + formatter.rs emit @echo (round-trip). 133 lib tests, fmt/clippy green. RENAME: full julia-the-viper→jtv slug + Julia the Viper→JtV prose across the repo (PR #47 merged) + nextgen-languages catalogue (#87 merged, rebuilt after main dropped all submodules); etymology kept as a README/CLAUDE footnote; the GitHub Settings repo-rename is the user's remaining manual step. NEXT rung: grade in TypeAnnotation::Function (function-valued params) [LANDED 2026-06-18, prefix-marker syntax] (the @epi(...) surface LANDED 2026-06-18); value-level semantics beyond τ=int (gap-005)"
 
@@ -50,7 +50,7 @@ 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). 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 (the float-locals CarrierEnv inference gate landed 2026-06-18)" },
+  { id = "gap-005", description = "Semantic model is Int-only: the 7 number systems are typed but stated-unproven at the value level (see ADR-0007 D6 + PROOF-CAPABILITY-MATRIX.adoc). PARTIAL 2026-06-18 (ADR-0010): per-system additive-algebra → Echo-tier CLASSIFICATION landed at proof/type/value level (JtvEcho SECTION 6, echo.rs carrier_echo, number.rs Value::reversal_echo). PARTIAL 2026-06-21: type_preservation lifted past τ=int to the whole integer-represented family {int,hex,binary} (these share the Int carrier; generalised via JtvType.isIntRepr; type_preservation_int recovers τ=int; #print axioms ⇒ no axioms). Remaining open half: value-level semantics for the carrier-DISTINCT systems float/rational/complex/symbolic", severity = "medium", status = "known", follow-up = "value-level semantics for float/rational/complex/symbolic (need their own value carriers; int/hex/binary done 2026-06-21)" },
   { 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" }
 ]
 
@@ -91,7 +91,8 @@ sessions = [
   { date = "2026-06-18", subject = "Float-locals soundness slice (typechecker carrier-aware gate). Echo admissibility is checked at the reverse-block site inside check_control_stmt, where self.env already holds the INFERRED types of params + prior local assignments — so typechecker.rs check_echo_admissible{,_with_residue} now build a CarrierEnv from self.env (Type→BasicType for the 7 numeric Types; non-numeric/Any omitted → default Int=Safe) and call echo::classify_stmts_in_env. Effect: a reverse{} over a float LOCAL (typed only by inference, e.g. x = 2.5) is correctly REJECTED under Safe-only (was wrongly Safe-admitted); reversible{}->tok still admits it (token retains the rounding residue). Contained change (no reordering, no new inference pass). 4 typechecker tests (float carrier rejected; inferred-float-local rejected end-to-end; int contrast ok; float reversible-tok admitted). ADR-0010 §Status/§Consequences/§Open updated (slice landed; remaining minor corner = carrier-awareness inside reversible-if branches). cargo fmt/clippy/test green (127 lib tests; cleared a clippy approx_constant deny on a 3.14 literal → 2.5). Whole-suite check: no existing test/example relied on a float reverse{} being accepted, so the stricter rule broke nothing." },
   { date = "2026-06-18", subject = "Surface Echo grades (ADR-0009 D1) — Bundle A (parameterised syntax + upper-bound policy). @echo(Safe|Neutral|Breaking) annotation on functions: grammar.pest echo_marker = '@echo' '(' echo_grade ')' and function_decl markers now (purity_marker|echo_marker)*; parser.rs consumes leading markers in a loop (order-independent with @pure) → FunctionDecl.echo_annotation. The Echo enum moved echo.rs→ast.rs (gains Serialize) with a `pub use crate::ast::Echo` re-export in echo.rs to break the ast↔echo cycle so FunctionDecl can hold it; all `echo::Echo` sites unchanged. UPPER-BOUND check typechecker.rs check_echo_annotations (3rd pass of check_program): inferred ⊑ annotated against the carrier-aware call-graph-composed effect.rs resolved_effects — a function may declare MORE loss than it incurs, never less (modular: caller checks against callee's declared ceiling). The reverse-gate still uses the ACTUAL inferred grade, so an annotation can't loosen reversal soundness. pretty.rs + formatter.rs emit @echo after purity (round-trip fidelity, pinned by a pretty round_trip test). 6 new tests (2 parser incl. either-order, 3 typechecker accept/reject/absent, 1 round-trip); 133 lib tests, fmt/clippy green. effect.rs header note refreshed. REMAINING: grade in TypeAnnotation::Function (function-valued params) [LANDED 2026-06-18, prefix-marker syntax]; parallel @epi(...) surface." },
   { date = "2026-06-18", subject = "@epi(...) epistemic-grade surface (ADR-0009 D2) — mirror of the @echo surface. @epi(Opaque|Partial|Transparent) annotation on functions: grammar.pest epi_marker; parser.rs marker loop also consumes epi_marker → FunctionDecl.epi_annotation (order-independent with @pure/@echo). Epistemic enum moved epistemic.rs→ast.rs (gains Serialize) with `pub use crate::ast::Epistemic` re-export, same cycle-break as Echo. typechecker.rs check_echo_annotations renamed check_effect_annotations: now checks BOTH axes (inferred.echo ⊑ @echo, inferred.epi ⊑ @epi) against resolved_effects (FunctionEffect carries .echo + .epi). pretty.rs + formatter.rs emit @epi after @echo. 5 new tests (parser @epi + echo&epi-together, typechecker epi accept/reject, round-trip); 138 lib tests, fmt/clippy green. Completes the ADR-0009 D1+D2 function-DECLARATION effect surface. REMAINING on this axis: carry the (echo,epi) row in TypeAnnotation::Function (function-VALUED params) — has a function-type grade-syntax + variance design choice to settle." },
-  { date = "2026-06-18", subject = "Function-TYPE grade carrying (ADR-0009 D1/D3) — completes the ADR-0009 effect surface. A function type Fn(...) -> T may now carry the (echo,epi) row with PREFIX markers (user choice): @echo(Neutral) @epi(Partial) Fn(Int) -> Int. ast.rs: new EffectGrade { echo: Option<Echo>, epi: Option<Epistemic> } (Default); TypeAnnotation::Function gains a trailing EffectGrade; typechecker Type::Function likewise. grammar.pest function_type now (echo_marker|epi_marker)* ~ 'Fn' ...; parser splits the leading markers from the param/return type_annotations. annotation_to_type carries the grade into Type::Function; Display + pretty.rs + formatter.rs emit the prefix markers (round-trip). coercible_to gains a function-type case: COVARIANT in the grade (grade_leq — a function that loses/reveals LESS is usable where MORE is allowed; None target = unconstrained; None source can't satisfy a Some ceiling; params/return invariant for now). 4 tests (parse graded + ungraded; round-trip; covariance accept/reject/unconstrained); 142 lib tests, fmt/clippy green. HONEST SCOPE: representational/forward-infrastructure — JtV has no first-class function VALUES (no lambdas/indirect calls) yet, so the value-against-type coercion is correct but LATENT until function values land. ADR-0009 D1+D2+D3 declaration+type effect surface now COMPLETE." }
+  { date = "2026-06-18", subject = "Function-TYPE grade carrying (ADR-0009 D1/D3) — completes the ADR-0009 effect surface. A function type Fn(...) -> T may now carry the (echo,epi) row with PREFIX markers (user choice): @echo(Neutral) @epi(Partial) Fn(Int) -> Int. ast.rs: new EffectGrade { echo: Option<Echo>, epi: Option<Epistemic> } (Default); TypeAnnotation::Function gains a trailing EffectGrade; typechecker Type::Function likewise. grammar.pest function_type now (echo_marker|epi_marker)* ~ 'Fn' ...; parser splits the leading markers from the param/return type_annotations. annotation_to_type carries the grade into Type::Function; Display + pretty.rs + formatter.rs emit the prefix markers (round-trip). coercible_to gains a function-type case: COVARIANT in the grade (grade_leq — a function that loses/reveals LESS is usable where MORE is allowed; None target = unconstrained; None source can't satisfy a Some ceiling; params/return invariant for now). 4 tests (parse graded + ungraded; round-trip; covariance accept/reject/unconstrained); 142 lib tests, fmt/clippy green. HONEST SCOPE: representational/forward-infrastructure — JtV has no first-class function VALUES (no lambdas/indirect calls) yet, so the value-against-type coercion is correct but LATENT until function values land. ADR-0009 D1+D2+D3 declaration+type effect surface now COMPLETE." },
+  { date = "2026-06-21", subject = "type_preservation lifted past τ=int to the integer-represented family {int,hex,binary} (gap-005 partial). LOCAL LEAN TOOLCHAIN UNBLOCKED: elan 4.2.2 was present but had no toolchain, and `release.lean-lang.org` is off the egress allowlist (its 'Host not in allowlist' page is the stray 'H' that broke elan's release-metadata parse). Bypassed by fetching the v4.12.0 linux tarball straight from GitHub releases (github.com + the asset host ARE allowlisted) and unpacking it into ~/.elan/toolchains/leanprover--lean4---v4.12.0 — elan then recognises the pinned toolchain; full `lake build` exit 0 (suite is mathlib-free, zero packages, no network). PROOF (JtvTypes.lean SECTION 6): inductive TypedValue gains hex + binary constructors (all three number systems share the Int runtime carrier — hex/binary ARE int-represented); new predicate JtvType.isIntRepr {int,hex,binary}↦True else False; type_preservation generalised from `τ=int → …` to `(hτ : τ.isIntRepr) → TypedValue (evalDataExpr e σ) τ`, proved `cases τ <;> first | exact TypedValue.{int,hex,binary} | simp only [JtvType.isIntRepr] at hτ`; type_preservation_int corollary recovers the original τ=int statement (via subst + trivial). `#print axioms` ⇒ BOTH new theorems depend on NO axioms. INVARIANTS held: full lake build exit 0; 0 sorry/admit/axiom (word-boundary grep); 0 True-typed theorems. DOCS synced: PROOF-CAPABILITY-MATRIX (scope-of-model rewrite + new key-theorems row + 'checked 2026-06-04; re-verified 2026-06-21' note), ADR-0007 consequence #1, ADR-0010 §gap-005 + §Open. float/rational/complex/symbolic REMAIN stated-unproven (distinct carriers, each needs its own value model). NOTE for next session: the local toolchain at ~/.elan is ephemeral (container reclaimed on inactivity) — re-run the GitHub-releases bypass to restore `lake build`; CI (proof-regression.yml) is the durable verifier." }
 ]
 
 [design-artefact-locations]

@@ -171,11 +171,13 @@ basis for the v2 `(c)` Neutral bridge and the number-system → tier map.
 
 . *Number-system semantics work (next-but-one priority).* The Lean model
   is currently `Int`-only (`evalDataExpr : DataExpr → State → Int`);
-  the seven systems are *typed* but `stated-unproven` at the value
-  level, and `type_preservation` is mechanised only for `τ = int`. The
-  semantics layer must (a) give each system a value model, (b) classify
-  each by its additive algebra → Echo tier per D6, and (c) keep
-  addition-only (D1) — `×`/`÷` generated, not primitive.
+  the carrier-distinct systems (`float`/`rational`/`complex`/`symbolic`)
+  are *typed* but `stated-unproven` at the value level. `type_preservation`
+  is mechanised for the whole *integer-represented family* `{int, hex,
+  binary}` (these share the `Int` carrier; generalised via `isIntRepr`,
+  zero axioms). The semantics layer must (a) give each remaining system a
+  value model, (b) classify each by its additive algebra → Echo tier per
+  D6, and (c) keep addition-only (D1) — `×`/`÷` generated, not primitive.
 . *v2 "(c)" bridge (LANDED 2026-06-15).* Implements the Neutral tier of
   D5: `reverse { }` stays Safe-only; `reversible { } -> tok` admits
   Neutral via the retained log/token (Bennett). Lean: `JtvEcho`

@@ -137,7 +137,11 @@ The algebra -> tier map has a single home and is mirrored, not duplicated:
   residue). Closes the gap this ADR previously flagged.
 . *`gap-005` partially addressed:* the seven systems are now *classified* by
   additive algebra at type and value level. The orthogonal half — lifting
-  `type_preservation` semantics beyond `τ = int` — remains open.
+  `type_preservation` semantics beyond `τ = int` — is now done for the whole
+  *integer-represented family* `{int, hex, binary}` (hex/binary share the `Int`
+  carrier, so the generalised `type_preservation` covers them via `isIntRepr`;
+  zero axioms). It remains open for `float`/`rational`/`complex`/`symbolic`,
+  which need their own value models.
 
 == Open / deferred
 
@@ -150,7 +154,8 @@ The algebra -> tier map has a single home and is mirrored, not duplicated:
   (idempotent) system is added, give it its `NumAlgebra` level and the
   Neutral/Breaking tier follows; no spine re-proof.
 * *Value-level semantics (`gap-005`).* `type_preservation` / round-trip proofs
-  for `τ ≠ int`.
+  for the carrier-distinct systems `float`/`rational`/`complex`/`symbolic`
+  (the int-represented family `{int, hex, binary}` is now covered).
 
 == References
 

@@ -420,20 +420,63 @@ theorem total_no_loops (s : ControlStmt) (h : s.respectsPurity Purity.total = tr
 -- SECTION 6: TYPE SOUNDNESS
 -- ============================================================================
 
-/-- Typed values: runtime values with their types -/
+/-- Typed values: runtime values with their types.
+
+    `int`, `hex`, and `binary` share the same `Int` runtime carrier —
+    hex and binary are int-represented (see `JtvType`) — so an evaluated
+    `Int` legitimately inhabits any of the three. The remaining number
+    systems (`float`/`rational`/`complex`/`symbolic`) have distinct
+    runtime carriers that the `Int`-only evaluation model does not build,
+    so they are deliberately absent here (see PROOF-CAPABILITY-MATRIX
+    §"Scope of the semantic model"). -/
 inductive TypedValue : Int → JtvType → Prop where
-  | int : ∀ n, TypedValue n JtvType.int
+  | int    : ∀ n, TypedValue n JtvType.int
+  | hex    : ∀ n, TypedValue n JtvType.hex
+  | binary : ∀ n, TypedValue n JtvType.binary
+
+/-- The integer-represented type family: exactly the `JtvType`s whose
+    runtime values are plain `Int`s (`int`, `hex`, `binary`). These are
+    the types for which `type_preservation` holds under the `Int`-only
+    evaluation model. -/
+def JtvType.isIntRepr : JtvType → Prop
+  | JtvType.int    => True
+  | JtvType.hex    => True
+  | JtvType.binary => True
+  | _              => False
 
 /--
-  **Theorem (Type Preservation)**:
-  If Γ ⊢ e : τ and e evaluates to v, then v has type τ.
+  **Theorem (Type Preservation, integer-represented family)**:
+  If `Γ ⊢ e : τ` with `τ` an integer-represented type (`int`, `hex`, or
+  `binary`) and `e` evaluates to `v`, then `v` has type `τ`. Because the
+  three int-represented types share the `Int` carrier, the evaluated
+  value inhabits whichever of them the type system assigned.
+
+  This lifts the previous `τ = int` mechanisation to the full int-
+  represented family; `float`/`rational`/`complex`/`symbolic` remain
+  `stated-unproven` at the value level pending their own evaluation
+  models (they do not share the `Int` carrier).
 -/
 theorem type_preservation (Γ : TypeEnv) (e : DataExpr) (τ : JtvType) (σ : State)
-    (_h : DataTyping Γ e τ) :
-    -- For integer types, the result is an integer
+    (_h : DataTyping Γ e τ) (hτ : τ.isIntRepr) :
+    TypedValue (evalDataExpr e σ) τ := by
+  cases τ <;>
+    first
+      | exact TypedValue.int (evalDataExpr e σ)
+      | exact TypedValue.hex (evalDataExpr e σ)
+      | exact TypedValue.binary (evalDataExpr e σ)
+      | simp only [JtvType.isIntRepr] at hτ
+
+/--
+  **Corollary**: the original `τ = int` preservation statement, recovered
+  from the int-represented-family theorem. Kept so the `int`-only claim
+  remains directly citable.
+-/
+theorem type_preservation_int (Γ : TypeEnv) (e : DataExpr) (τ : JtvType) (σ : State)
+    (h : DataTyping Γ e τ) :
     τ = JtvType.int → TypedValue (evalDataExpr e σ) JtvType.int := by
-  intro _hτ
-  exact TypedValue.int (evalDataExpr e σ)
+  intro hτ
+  subst hτ
+  exact type_preservation Γ e JtvType.int σ h trivial
 
 /--
   **Theorem (Progress for Typed Terms)**: