proof(types): lift type_preservation past τ=int to the int-represented family {int, hex, binary}

[hyperpolymath]

What

Lifts type_preservation (JtvTypes.lean SECTION 6) from τ = int to the whole integer-represented family {int, hex, binary}.

Under the Int-only evaluation model, hex and binary share the same runtime carrier as int (they are int-represented — see the JtvType constructor comments), so an evaluated Int legitimately inhabits any of the three.

Changes (Lean)

• TypedValue gains hex / binary constructors alongside int.
• New predicate JtvType.isIntRepr picks out {int, hex, binary}.
• type_preservation generalised from τ = int → … to:

  (hτ : τ.isIntRepr) → TypedValue (evalDataExpr e σ) τ

  proved by 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).

Verification (local + CI)

Verified locally under the pinned leanprover/lean4:v4.12.0 toolchain:

• full lake build exit 0 (suite is mathlib-free, zero packages)
• grep -rnwE 'sorry|admit|axiom' ⇒ 0 across all eight libraries
• 0 True-typed theorems
• #print axioms type_preservation and …_int ⇒ does not depend on any axioms

proof-regression.yml re-runs lake build on every jtv_proofs/** change as the durable check.

Honest scope

float / rational / complex / symbolic remain stated-unproven at the value level — they have distinct runtime carriers (not Int) and each needs its own value model. This PR closes only the int-represented slice of gap-005.

Docs synced

• PROOF-CAPABILITY-MATRIX.adoc — scope-of-model rewrite, new key-theorems row, "re-verified 2026-06-21" note
• ADR-0007 consequence ci(antipattern): allowlist legit TS bridge/adapter paths #1, ADR-0010 §gap-005/§Open
• STATE.a2ml session history + gap-005 status

🤖 Generated with Claude Code

---

Generated by Claude Code