Lean 4
把二次域当作坐标系来计算
QuadraticNumberFields 的核心，是让 QuadraticField、QuadraticFieldCat 和 Qsqrtd d 各司其职：抽象表达、范畴组织、具体计算。
问题不只是定义 ℚ(√d)
在纸上，二次域常常写成 ℚ(√d)，其中 d 是平方自由整数。但在 Lean 里，难点并不只是把这个对象写出来，而是让参数变化、域同构、整数环、判别式和素理想分裂都能被统一管理。
如果一开始就把“二次域”定义成等价类，数学上也许优雅，但计算会被商结构拖慢。做 trace、norm、整性和判别式时，我们需要能展开元素、使用坐标、让 Lean 直接计算。因此这个项目的核心策略是：先保留标准坐标模型，再把抽象性作为外层结构加上去。
三层对象
第一层是 `QuadraticField K`：它应该表达 K 是 ℚ 上的二次扩张。这一层是性质，不是坐标模型。它回答的问题是：一个给定的域 K 是否具有二次域结构？
第二层是 `QuadraticFieldCat`：它把满足这个性质的域打包成范畴对象，态射是 ℚ-代数同态。这一层负责组织对象、同构、函子和自然性。
第三层是 `Qsqrtd d`：它是标准模型 ℚ(√d)，也是项目里最适合计算的地方。整数环分类、判别式公式、实/虚二次性和分裂行为都应当优先在这里证明。
为什么不是先做等价类
二次域当然应该按同构分类；例如 ℚ(√d) 与 ℚ(√d') 是否同构，取决于 d'/d 是否是有理平方。但这类分类定理更适合作为桥梁，而不是作为底层定义。
底层定义如果是等价类，每次计算都要面对代表元选择和商上的下降问题。相反，在 `Qsqrtd d` 上可以直接计算，再用分类定理说明不同参数给出的对象什么时候相同。这保留了坐标模型的可计算性，也保留了抽象分类的正确语义。
Qsqrtd 和抽象二次域之间的桥
`Qsqrtd.rescale` 应该被提升成系统性的结构：对每个有理数单位 a，有一个从 `Qsqrtd d` 到 `Qsqrtd (a² d)` 的 ℚ-代数等价。进一步说，这些 rescale 等价应当组成自然的、可复用的接口，而不是散落在证明里的手工 RingEquiv。
同样，任意 `Algebra.IsQuadraticExtension ℚ K` 都应当能通过某个标准参数 d 与 `Qsqrtd d` 联系起来。于是项目的证明路线就是：在标准模型上算清楚，再通过同构把结论搬运到抽象 K。
最终目标
这个项目真正要形式化的，不只是几个二次域的例子，而是一套二次域的工作语言。`Qsqrtd d` 是坐标，`QuadraticField K` 是抽象性质，`QuadraticFieldCat` 是管理和运输结果的范畴层。
这样组织之后，整数环分类、判别式、实嵌入个数、以及素理想的 split/inert/ramified 三分，都可以先在可计算模型中完成，再提升成不依赖具体坐标的结论。这也是我认为 QuadraticNumberFields 的核心思想：坐标优先，分类作桥，抽象收尾。