本仓库是 Graph Opt Verify 的 Lean 模块快照，供 AI 和研究者阅读源码，设计从当前受限理想代数语义到更完整实数语义的扩展方案。
任务与提示词：PROMPT.txt。架构说明：ARCHITECTURE.md。
给定优化前后的 ONNX 子图，我们生成 Lean 中的两张图，证明对所有合法输入，两图的完整输出相同。现在数值定义主要要求 Semiring R，能处理部分矩阵算术和布局操作，但缺少除法、指数、对数、归一化等精确语义。
我们希望得到一份有源码依据的设计：如何复用现有图执行和证明框架，扩展到理想实数 ℝ，支持更多真实算子与优化，并尽量证明参数化张量定理。理想实数运算与 IEEE 浮点逐步舍入的结论需要分别说明。
当前 226 个最新 ONNX 算子可进入参数化图表示，其中 18 类有受限的精确定义；具体支持范围见 operator-support.json。IdealReal.lean 目前只有接口占位。
| 顺序 | 源码 | 解决的问题 |
|---|---|---|
| 1 | Core/Value.lean、Core/IdealTensor.lean | FLOAT 如何解释为抽象张量，INT64 控制量如何精确解码 |
| 2 | Core/Relation.lean | 算子合法域、输入输出关系、版本化解释与确定性 |
| 3 | Core/Graph.lean、Core/GraphEquiv.lean、Core/GraphProgram.lean | 节点执行、整图执行及图等价定理 |
| 4 | Ops/TensorRelations.lean、Ops/ExtendedRegistry.lean | 当前实际支持的算子语义和注册范围 |
| 5 | Ops.lean、Rules.lean、Ops/IndexMaps.lean | 可复用的数学函数、融合定理与索引证明 |
| 6 | Scalar/IdealReal.lean、Scalar/Profiles.lean | 实数扩展的现有接口与数值标签 |
| 7 | relational_tensor_codegen.py | 如何生成含实际图执行的 Lean 证书 |
| 8 | ReshapeComposition.lean、QKVFusion.lean | 两份已生成的完整证明实例 |
Ops/SchemaRelations.lean 和 Ops/AllSchemas.lean 展示参数化解释。Generated/SchemaCatalog.lean 是生成的版本目录，按需查询即可。Tests/ 中保留库级正负检查。
GraphOptVerify/、GraphOptVerify.lean：完整项目 Lean 源码及其本地 import 依赖。lakefile.toml、lake-manifest.json、lean-toolchain：原工程固定的 Lean/Mathlib 4.19.0 配置。integration/graphopt/：与解释选择、图生成和证书检查直接相关的 Python 源码摘录，供架构阅读；未包含完整 Python CLI 及其全部依赖。examples/：连续 Reshape 合并和 QKV 融合的历史生成证书，均含辅助等式和最终图定理。support/：逐算子支持范围。SOURCE_MANIFEST.json：来源 revision、逐文件哈希和示例来源，便于核对快照。
在已准备 Lean 4.19.0 与依赖的环境中，可从本目录执行：
lake build GraphOptVerify.Tests.Relational GraphOptVerify.Tests.TensorRelations
lake env lean examples/ReshapeComposition.lean
lake env lean examples/QKVFusion.lean本次发布只核对源码复制、import 完整性及文档链接，没有重新运行 Lean。两份示例来自原项目已有的 v7 认证记录，不包含原 ONNX 模型与完整认证包；它们用于展示命题和证明的实际结构。
原项目的优化器追踪、Candidate 提取、实验日志和长篇历史文档不在这个阅读包内。Lean 的输入是已经提取出的两侧图，理解本次实数建模问题不需要上游算法。