principal_ideal_eq_of_mutual_dvd
plain-language theorem explainer
In a commutative ring, mutual divisibility of elements a and b forces the principal ideals they generate to coincide. Recognition Science cites this algebraic identity as the core step for IMC equality templates in BSD Stage 6. The proof reduces ideal equality to membership checks and constructs the required multipliers directly from the two divisibility witnesses.
Claim. In a commutative ring $R$, if $a$ divides $b$ and $b$ divides $a$, then the principal ideal generated by $a$ equals the principal ideal generated by $b$.
background
Module PinchAlgebra develops tools for mutual divisibility and Fredholm obstructions under Foundation paper F5, with primary citations to BSD and secondary use in Yang-Mills. The local setting treats principal ideals Ideal.span {a} inside CommRing R and the relation a ∣ b as the basic algebraic currency for later operator pinch arguments. The supplied doc-comment states the claim directly: in a commutative ring, (a) = (b) iff a | b and b | a. Upstream structures such as reversal maps on Fin 8 and integration-gap constants supply auxiliary notation but are not invoked in the argument itself.
proof idea
The proof is a direct term-mode verification. It applies ideal extensionality, reduces membership to the singleton-span predicate, and splits into two directions. Each direction extracts the divisor witness (c from hba, d from hab) and multiplies the generator by that witness, then rewrites using the given equality and ring axioms to obtain the required element.
why it matters
The declaration supplies the single step used by imc_equality_template, which the downstream doc-comment calls the algebraic heart of BSD Stage 6. It completes the mutual-divisibility case inside F5 Pinch Algebra, enabling the transition from one-sided Kato-type equalities to full ideal equality. In the broader framework this identity supports the operator forms needed for the eight-tick octave and D = 3 forcing steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.