Formal Verification
Isabelle/HOL：现代子模贪心算法形式化
一个覆盖 classical greedy、LazyGreedy 与 StochasticGreedy 的 Isabelle/HOL formalization 对象。
Status:核心定理线完成正在 clean-up、依赖整理与 AFP 风格打磨
代表性工作
这一页只回答一个问题：我具体做出了什么对象。
这里不再重复研究叙事，只保留对象、状态和材料入口。Research 负责讲问题线，Work 负责给证据。
Work
This page answers one question: what concrete objects I have made.
The research narrative stays on the Research page. Here the emphasis is only on the object, its current status, and where the materials live.
Selected Work
Selected Work
Duality / Invariance
不变性下的对偶与结构分数
围绕 dual collapse、Range(B) 与 inconsistency score 的一组推导、阶段性笔记与公开归档。
Status:进行中正在把 collapse 后剩下的结构组织成更稳定的对象
Prototype
Metalcore Piano Lab
一个把音频 / MIDI 映射到可玩 chart events 的浏览器原型。
Status:Work in progress持续检验离散化与可玩性约束
Formal Verification
Isabelle/HOL: modern submodular greedy formalization
An Isabelle/HOL object covering classical greedy, LazyGreedy, and StochasticGreedy.
Status:Core theorem lines completeCurrent work is clean-up, dependency refinement, and AFP-style presentation
Duality / Invariance
Duality and structural scoring under invariance
A developing set of derivations, notes, and public archives around dual collapse, Range(B), and inconsistency scoring.
Status:OngoingThe current task is to organize what survives after collapse into a more stable object
Prototype
Metalcore Piano Lab
A browser prototype that maps audio / MIDI into playable chart events.
Status:Work in progressStill tightening discretization and playability constraints