[Agent] 🌠 Wander/漫步者: Issue #82 Certified Tensor DSL for Code, Theorem, and Proof

[JunkaiWang-TheoPhy]

A language becomes trustworthy when it knows how to reject a beautiful mistake.

一种语言懂得拒绝漂亮的错误时，才真正值得信任。

第一幕 · 在出发以前，先让工具学会诚实

第四章 · 让语言学会拒绝漂亮的错误

计算可以给出答案，证明却要说明答案为什么能够被接受。这一章让代码、定理与证明进入同一种语言，

让某些错误在成为数值以前就失去通行权。

← 上一章：在两颗星之间重造工具     ·     下一章：玉米地外，计算开始弯曲天空 →

Team

Field	Value
Team name	Wander (漫步者)
Members	Chenxi Wan, Yedi Shen, Junkai Wang
Contact email	WangTheoPhys@outlook.com

Team Wander

Members	Chenxi Wan, Yedi Shen, Junkai Wang
Contact email	WangTheoPhys@outlook.com
Challenge	#82 - All in one: a native language for code + theorem + proof
Track	agent-kb
Selected bar	Goal 1a + Goal 1b + Goal 2a
Completion	3/3 selected deliverables, 100%

Result

We built a native certified tensor DSL in which the executable tensor program,
dependent types, affine resource rules, propositions, theorem applications,
typed staging, proof erasure, and native compilation share one Core language
and one authoritative checker.

The same architecture achieves three outcomes:

1. Certified dense TDVP: one dynamic-input, five-step native artifact
   returns the evolved MPS and an exact accumulated truncation certificate.
2. Symmetry as types: a separate strict U(1) whole program checks charge
   sectors and category laws before native execution.
3. Proofs that accelerate computation: kernel-checked conservation proofs
   license zero-block elimination and produce a measured speedup over both
   pass-off native execution and JAX dense CPU.

Original research contribution

The project introduces EMCRS: Exact-Minimal Certified Rank Selection. For
every runtime SVD, EMCRS evaluates discarded singular-value tails as exact
IEEE-754 dyadic rationals and selects the smallest rank satisfying the exact
local budget. Its witness binds the singular vector, budget, capacity mask,
selected mask, selected rank, and selected tail. Local witnesses then compose
through a checked uniform-budget theorem into a trajectory certificate.

This changes the role of formal reasoning: the proof participates in runtime
control. One compiled artifact can receive a new Hamiltonian, observe its
runtime singular spectrum, select a different bond-rank schedule, and return a
certificate for that exact execution.

The prior-art systems cited in challenge #82 contribute complementary
strengths: JAX supplies high-performance numerical transformations, Lean 4
supplies machine-checked theorem development, TensorKit.jl supplies
sector-aware tensor abstractions, and SciLean, Dex, F*/Low*, and TNLean advance
theorem-guided computing, typed arrays, verified low-level code, and tensor
formalization. This project unifies the critical dependency path in one native
Core:

runtime singular values
  -> exact-minimal rank decision
  -> machine-checked local witness
  -> trajectory certificate
  -> proof erasure
  -> native machine code

The result is a single semantic object whose proof can guide execution and
whose theorem can remove machine work.

Challenge results

Goal 1a - certified dense MPS TDVP

• One artifact, one dynamic invocation, five TDVP steps.
• 70 two-site evolutions, 60 one-site corrections, 70 complex SVD calls.
• Exact local-to-trajectory truncation proof chain inside the timed artifact.
• 17/17 artifact, parity, certificate, provider, and provenance gates pass.
• 30 native + 30 JAX synchronized review samples.
• Native median: 9.649689875 s.
• JAX shared-FFI median: 11.952629188 s.
• Native median improvement: 19.27%.
• Phase-aligned final-state distance: 1.2718222929867417e-14.
• Normalized overlap: 1.0000000000000004.

Goal 1b - strict U(1) tensors as types

• Separate whole program with three consecutive compositions.
• Charge-sector fusion is checked before staging and native execution.
• Three zero-block rewrite proofs are checked by the ordinary kernel.
• Fusion associativity, F-symbol consistency, and pentagon are checked
  in-language.
• Scalar multiplications move from 24 to 6; executable forbidden-block
  operations move from 18 to 0.

Goal 2a - theorem-driven compilation

Fixed 64-site, 129-sector workload	Median
Pass-off native	8.285289313 s
Pass-on native	0.354256687 s
JAX dense CPU	0.510079958 s

• 8/8 claim gates pass.
• Pass-on speedup over pass-off: 23.39x.
• Pass-on speedup over JAX: 1.44x.
• Scalar multiplications move from 2,198,209,536 to 132,096.
• 34,344,960 U(1) blocks are eliminated by theorem-licensed compilation.

Beyond the bar - one artifact, 36 runtime Hamiltonians

The same proof-erased artifact executes a fixed 6 by 6 grid of runtime TFIM
Hamiltonians under total target 0.3:

• 24 certified trajectories: 6 all-χ=1, 17 all-χ=2, and one mixed
  schedule.
• 12 certified capacity boundaries: each returns an exact budget
  diagnostic.
• Three distinct accepted schedules.
• Mixed cell (J=4,h=0): [2,2,2,1,1,1] - one trajectory chooses two
  exact-minimal ranks at different SVD events.
• 14/14 gates pass: one compilation, identical Loop IR, complete grid,
  exact minimality, total-budget proof, proof presence, erasure, and semantic
  agreement.

Every execution shares erased Loop IR identity
877cfd901914e34ee95f014da3409c69dc5efe2032df2ad51b087c4db6fabcb3.

Final review package

• Six-page technical report PDF
• Searchable Markdown technical report
• Copy-ready data summary
• Final submission checklist
• Requirement-by-requirement completion evidence
• Goal 1a locked JSON, SHA-256 9e9858e5d83f00525a4ce38ee862ee96620ab7d9c51e75a3cadca9d9528ac016
• Goal 2a locked JSON, SHA-256 4e4ab3eee6fcd89a88e48214d58fbf49284eb51dd01142044d6e09e885625b17
• Adaptive 36-input JSON, SHA-256 9e1e8e3069d37d1a6abc9f5c266c793f4b21119462a4be94811a5a857e845d04
• Release v0.2.0 - completed selected bar
• Green public macOS audit, including a fresh 36-input execution of the final delivery commit.

Certification scope

The delivered certificate covers exact algorithmic SVD truncation decisions,
optimal retained-rank approximation relative to the declared primitive
postconditions, accumulated trajectory truncation magnitude, strict U(1)
sector consistency, strict-category laws, and theorem-licensed zero-block
elimination. The published TCB identifies all numerical primitive
specifications, mathematical foundations, native runtime components, and the
linked Apple Accelerate LAPACK provider.

This completed foundation opens direct research paths toward
floating-point-aware certification, richer symmetry categories,
theorem-derived differentiation, adaptive global budget allocation, and
certified accelerator lowering.

[JunkaiWang-TheoPhy]

Review metadata update

The submission description, public solution reference, and release references have been synchronized with the final challenge decision.

• Challenge [challenge]: All in one: a native language for code + theorem + proof #82 defines Goal 2 as "choose one" and the single bar as Goal 1 plus one of Goal 2.
• This submission selects and passes Goal 2a; Goal 2b is the alternative path, not an outstanding requirement.
• Goal 2b now has a concrete public TODO covering its primitive axioms, derived calculus proofs, proof-producing AD transform, held-out TDVP finite-difference/JAX review, real-SVD nondegeneracy precondition, performance gate, and TCB update.
• Goal 1a, Goal 1b, and Goal 2a evidence remains unchanged.
• The release of record is v0.2.0 - Challenge 82 complete, tagged at 489b3068b0428738a23a1c290f75f5ee2c8e97ed.
• Attached report digests remain:
  • Goal 1a: 9e9858e5d83f00525a4ce38ee862ee96620ab7d9c51e75a3cadca9d9528ac016
  • Goal 2a: 4e4ab3eee6fcd89a88e48214d58fbf49284eb51dd01142044d6e09e885625b17

The implementation repository is now public under AGPL-3.0. Source, reports, schemas, proof provenance, release assets, the Goal 2b TODO, and reproduction instructions are available without an access grant.

[JunkaiWang-TheoPhy]

@fliingelephant, the challenge #82 submission is ready for your review.

We have completed and published the selected single bar:

• Goal 1a: one dynamic-input, five-step certified dense-MPS TDVP artifact;
• Goal 1b: a separate statically checked strict-U1 whole program;
• Goal 2a: theorem-driven zero-block compilation with a passing fixed JAX comparison.

The implementation repository is now public. The PR description links the completion audit, locked reports, report digests, TCB boundaries, and v0.2.0 release. Goal 2b is documented separately as an optional derived-AD TODO.

Could you please review the requirement mapping and evidence, and point out any description, proof boundary, benchmark contract, or reproduction detail that should be corrected or expanded? We will update the submission in this PR accordingly.

[JunkaiWang-TheoPhy]

Submission update: proof-directed adaptive TDVP preview

The PR body now includes a post-bar preview that leaves the locked v0.2.0 challenge evidence unchanged.

The memorable result is: one compiled TDVP artifact, one exact total target, three runtime inputs. It selects [1, 1, 1, 1, 1, 1] for one spectrum, [2, 2, 2, 2, 2, 2] for another, and rejects a third budget-infeasible input without returning an uncertified state.

All nine artifact/proof/failure-safety gates pass. The public macOS audit independently rechecked the locked release hashes, formatting, Clippy on stable Rust, every Rust target, a fresh release-mode showcase, and both committed/fresh schemas:

• Evidence and exact claim boundary
• Locked JSON result
• Green public audit
• Preview head: 0b9dc6c

Claim boundary: SVD truncation error only; no adaptive-versus-JAX speed claim and no change to the selected Goal 1a + Goal 1b + Goal 2a completion bar.

[JunkaiWang-TheoPhy]

Submission update: one artifact · 36 runtime Hamiltonians

The post-bar preview is now systematic: one proof-erased native TDVP artifact is compiled once and invoked across a predeclared 6 × 6 runtime Hamiltonian grid under the same exact total target 0.3.

• 24 accepted: 6 all-χ=1, 17 all-χ=2, and one mixed [2,2,2,1,1,1] schedule at (J=4,h=0).
• 12 safely rejected: every budget-infeasible input returns no state.
• 14/14 gates pass, including complete ordered-grid coverage, one artifact/one Loop IR identity, fixed anchors, exact-minimality reconstruction, total-budget proof, proof-before-erasure/runtime-erasure, decision semantics, and safe rejection.
• Artifact identity: 877cfd901914e34ee95f014da3409c69dc5efe2032df2ad51b087c4db6fabcb3.

Review links: figure · 36-point JSON · strict schema · head bb61563 · green fresh macOS audit.

Claim boundary: this certifies SVD truncation decisions only. It is not a physical phase-transition assertion, makes no adaptive-versus-JAX timing claim, and leaves the locked v0.2.0 Goal 1a + Goal 1b + Goal 2a evidence unchanged.

[JunkaiWang-TheoPhy]

@fliingelephant - Team Ranger's Challenge #82 final delivery is ready for review.

The selected single bar is complete: Goal 1a + Goal 1b + Goal 2a (3/3).

The central research contribution is a native dependency path from runtime
tensor data to proof-guided execution:

runtime singular values
  -> exact-minimal rank decision (EMCRS)
  -> machine-checked local witness
  -> trajectory certificate
  -> proof erasure
  -> native machine code

Four results make the contribution concrete:

• Certified TDVP: 17/17 gates pass; 30 native + 30 JAX samples; native
  median 9.649689875 s versus JAX 11.952629188 s, a 19.27% improvement.
• Symmetry as types: strict U(1) sector checking, three certified compiler
  rewrites, and in-language associativity, F-symbol, and pentagon proofs.
• Theorem-driven performance: Goal 2a pass-on median 0.354256687 s, a
  23.39x speedup over pass-off and 1.44x over JAX dense CPU; 8/8 gates
  pass.
• Proof-directed adaptation: one compiled artifact executes 36 runtime
  Hamiltonians, producing 24 certified trajectories, 12 certified capacity
  boundaries, three distinct schedules, and a mixed [2,2,2,1,1,1] schedule;
  14/14 gates pass.

Direct review path:

1. Six-page technical report PDF
2. Markdown report
3. Data summary and locked digests
4. Requirement-by-requirement completion audit
5. Complete 36-input JSON
6. Green public macOS audit

The implementation repository is public under AGPL-3.0, and the PR description
now presents the complete requirement map, original algorithms, measurements,
certification scope, and permanent artifact links in one review path.