这一页只回答一个问题：我现在怎样理解这些问题。
我目前的研究线索并不是一个松散的兴趣列表，而是三条可以继续推进的问题主线：Isabelle/HOL、duality under invariance、以及 prototype / discretization。
下面每一条都用同一个模板来写，尽量把“问题意识”而不是“材料索引”放在前面；具体证据统一留给 Work 和 Notes。
This page answers one question: how I currently frame the problems.
My current work is organized not as a loose list of interests, but around three problem lines that can keep moving: Isabelle/HOL, duality under invariance, and prototype / discretization.
Each line below follows the same template so the emphasis stays on problem framing rather than on materials or navigation.
Question:如何把子模贪心算法的近似保证，连同算法构造、oracle-cost 叙事与后续扩展接口，一起组织成可持续发展的 Isabelle/HOL library？
Why it matters:我关心的不是“把一个 proof 搬进 proof assistant”这么简单，而是证明的结构、依赖与复用边界怎样在机器检验环境里被真正写清楚。
Current stage:classical greedy、LazyGreedy 与 StochasticGreedy 的核心 theorem line 已经成形；当前重点转向 clean-up、依赖整理与 submission-style presentation。
Next question:怎样把现有 development 收束成更稳定的接口，让它既能面向 AFP 风格展示，又不牺牲后续继续长新的能力？
Question:当一个 optimization model 因为 translation / gauge invariance 让最自然的 dual routes collapse 时，问题里到底还有没有可以恢复出来的 nontrivial structure？
Why it matters:如果 trivial lower bound 不是推导失误，而是模型结构本身导致的，那么真正有信息的对象可能不是 bound 本身，而是 collapse 之后剩下来的 structural score。
Current stage:我已经重新走通主要推导，并更清楚地看见 plain dualization 在哪里失去信息；现在留下来的，是一条和 Range(B)、cycle consistency 与 instance difficulty 相关的结构线索。
Next question:什么样的 gauge-fixing、augmentation 或更紧约束，能够把这条结构线索真正变成一个可解释、可比较、可延伸的 lower-bound 或 scoring object？
Question:把连续音频、节奏或事件流映射到可操作的离散对象时，哪些结构必须被保留，哪些约束只是为了方便实现？
Why it matters:这条线看起来更像 prototype work，但它和前两条其实问的是同一种事：一个对象被 formalize、dualize 或 discretize 之后，真正值得保留下来的结构到底是什么。
Current stage:浏览器原型已经搭起来，正在拿真实输入反复检验 onset、beat grid、alignment 与 playability constraints 这些假设在什么地方会失效。
Next question:怎样把“可玩性”从一组实现经验，进一步压缩成更明确的离散化准则与评估方式？
Question:How should the approximation guarantees, algorithmic constructions, oracle-cost narrative, and extension interfaces for submodular greedy algorithms be organized into an Isabelle/HOL library that can keep growing?
Why it matters:I am not only interested in moving a proof into a proof assistant, but in making the structure, dependencies, and reuse boundaries of that proof explicit enough to survive machine-checked development.
Current stage:The core theorem lines for classical greedy, LazyGreedy, and StochasticGreedy are in place; the current phase is clean-up, dependency refinement, and submission-style presentation work.
Next question:How should the current development be tightened into a more stable interface that is presentation-ready without losing its ability to support later extensions?
Question:When an optimization model collapses under translation or gauge invariance, is there still any nontrivial structure left to recover after the most natural dual routes fail?
Why it matters:If the trivial lower bound comes from the model rather than from a derivation mistake, then the informative object may no longer be the bound itself, but the structural score that remains after the collapse.
Current stage:I have reworked the main derivations and clarified where plain dualization loses information; what remains is a structural trail tied to Range(B), cycle consistency, and instance difficulty.
Next question:What kind of gauge-fixing, augmentation, or tighter constraints can turn that structural trail into a lower-bound or scoring object that is actually interpretable and reusable?
Question:When continuous audio, rhythm, or event streams are mapped into usable discrete objects, which structures must be preserved and which constraints are only implementation conveniences?
Why it matters:This looks more like prototype work on the surface, but it asks the same structural question as the other lines: what is actually worth preserving after an object has been formalized, dualized, or discretized?
Current stage:A browser prototype is already in place and is being stress-tested on real inputs to see where onset, beat-grid, alignment, and playability assumptions fail.
Next question:How can playability be compressed from a bundle of implementation heuristics into a clearer discretization criterion and evaluation scheme?
把页面从问题陈述带到可检查的材料，不让研究页只停在目录层。
From problem framing to inspectable materials, so the page does not stop at the level of a directory.
承接问题陈述的项目页、材料页与技术笔记入口。
Notes, repositories, and project pages that carry the evidence.
把 Isabelle/HOL、optimization prototype 与相关项目放在同一个可扫描入口里。
Projects, formal developments, and prototype work gathered into a single scannable entry point.
保留推导、形式化进展、失败路线和重新组织后的技术记录。
Derivations, formalization progress, failed routes, and reorganized technical records.
