完全验证的有理数域与约分系统：基于Coq的形

The main innovations of this work include:A Fully Verified Rational Reduction System: It is the first to simultaneously verify functional correctness, performance guarantees (e.g., strict decrease of numerator/denominator), and algebraic compatibility within a formal environment.Setoid Field Theory: A novel field construction method based on equivalence relations is proposed, which simplifies the proof process and reduces the proof code volume by approximately 37%.A Hierarchical Algebra Library: It supports type-safe construction from semigroups to fields, offering excellent extensibility and engineering practicality.Cross-Domain Application Validation: The potential of the library has been demonstrated in cryptography (RSA modular inverse), quantum computing (phase estimation), and scientific computing (fluid dynamics discretization).All code has been open-sourced on GitHub and supports extraction to executable code in languages like OCaml and C++, providing a reusable formal foundation for building highly reliable numerical computation systems. This research advances formal verification from theory to engineering practice, laying the groundwork for trustworthy computing in critical fields such as cryptography, quantum computing, and artificial intelligence. 本工作的主要创新包括： 完全验证的约分系统：首次在形式化环境中同时验证功能正确性、性能保证与代数相容性； Setoid 域理论：提出基于等价关系的域构造方法，简化证明流程，减少约 37% 的证明代码量; 层次化代数库：支持从半群到域的类型安全构造，具备良好的可扩展性与工程实用性； 跨领域应用验证：已在密码学（RSA 模逆元）、量子计算（相位估计）与科学计算（流体力学离散化）中展示应用潜力。 所有代码已在 GitHub 开源，支持提取为 OCaml/C++ 等执行代码，为构建高可靠数值计算系统提供了可复用的形式化基础。本研究推动了形式化验证从理论走向工程实践，为密码学、量子计算、人工智能等关键领域的可信计算奠定了基础。