Foundation Pinch Algebra Imc Equality Template

The equality template

In mathematics, two elements a and b of a ring are often compared by asking whether one divides the other. The declaration imc_equality_template captures a classical fact: if a divides b and b divides a, then the principal ideals they generate are equal. In plainer terms, each element is a multiple of the other, so the sets of all multiples of a and of b coincide. This is not a new discovery but a formalized, machine-checked restatement of a standard result in commutative algebra.

The template matters because it is a reusable proof pattern. Instead of proving equality of two ideals from scratch, a mathematician can show mutual divisibility and then invoke this template. The declaration is a theorem in the framework's machine-checked library, meaning its proof has been verified by a computer. It is a small but solid brick in a larger structure: the framework's paper F5 uses this template as the algebraic core of a strategy related to the Birch and Swinnerton-Dyer conjecture and to Yang-Mills theory. The template itself, however, does not depend on any of those larger goals; it stands alone as a general algebraic tool.

What the template does not claim is just as important. It does not assert that a equals b as elements, only that their principal ideals are equal. In a ring without zero divisors, mutual divisibility does imply the elements differ by a unit, but the template itself stops at the ideal level. It also does not claim anything about the specific rings or elements that appear in the BSD or Yang-Mills applications; it only provides the general lemma those applications would use. Finally, it is not a statement about the physical world. It is a piece of pure mathematics, a formal tool waiting for a context.

/-- **F5.2.3**: IMC equality from Kato (one side) + reverse divisibility (other side).
    This is the algebraic heart of BSD Stage 6.

    Given: (A) | (B) and (B) | (A) in a commutative ring,
    conclude (A) = (B) as principal ideals. -/
theorem imc_equality_template {R : Type*} [CommRing R]
    {A B : R} (hAB : A ∣ B) (hBA : B ∣ A) :
    Ideal.span ({A} : Set R) = Ideal.span {B} :=
  principal_ideal_eq_of_mutual_dvd hAB hBA

/-- **F5.1.2/1.4**: Principal ideal equality from mutual divisibility.
    In a commutative ring, (a) = (b) iff a | b and b | a. -/
theorem principal_ideal_eq_of_mutual_dvd {R : Type*} [CommRing R]
    {a b : R} (hab : a ∣ b) (hba : b ∣ a) :
    Ideal.span ({a} : Set R) = Ideal.span {b} := by
  ext x
  simp only [Ideal.mem_span_singleton]
  constructor
  · intro ⟨r, hr⟩
    obtain ⟨c, hc⟩ := hba
    exact ⟨r * c, by rw [hr, hc]; ring⟩
  · intro ⟨r, hr⟩
    obtain ⟨d, hd⟩ := hab
    exact ⟨r * d, by rw [hr, hd]; ring⟩

What this page does not claim

The template does not claim that a equals b as elements, only that their principal ideals are equal. It does not claim anything about the specific rings or elements in the BSD or Yang-Mills applications.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PinchAlgebra.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: