Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PinchAlgebra

show as:
view Lean formalization →

PinchAlgebra supplies the algebraic fact that in a commutative ring the principal ideal generated by a equals the one generated by b precisely when a and b divide each other. Workers on the foundation paper's F5 layer cite it when handling ideal structures ahead of topological arguments. The module consists of direct translations of standard ring lemmas drawn from Mathlib.

claimIn a commutative ring $R$, for $a,b \in R$ the principal ideals satisfy $(a)=(b)$ if and only if $a$ divides $b$ and $b$ divides $a$.

background

The module contains no new definitions and imports only Mathlib to access commutative-ring infrastructure. Its sole documented result is the standard equivalence between equality of principal ideals and mutual divisibility. The local setting is the algebraic substrate of the Recognition Science foundation layer, supplying tools that later modules apply to capacity and linking questions.

proof idea

This is a lemma module whose central statement follows directly from the definitions of principal ideals and divisibility; the remaining siblings are supporting facts on finite sets and equality templates.

why it matters in Recognition Science

The module feeds the TopologicalVeto module, which establishes the integer linking invariant only in D=3 as the main result of F6. It fills the F5.1.2/1.4 slot in the foundation paper and supplies the algebraic prerequisite for the topological capacity veto.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (4)