pith. sign in
module module high

IndisputableMonolith.Foundation.PinchAlgebra

show as:
view Lean formalization →

PinchAlgebra supplies commutative ring facts for ideal manipulations in the Recognition framework. Its central lemma equates principal ideal equality to mutual divisibility of generators. The module is invoked by the topological veto construction to control capacity in D=3. Proofs unfold directly from ideal membership and divisibility axioms with no auxiliary hypotheses.

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

PinchAlgebra provides the algebraic substrate for pinch operations and ideal-based constraints within Recognition Science. It imports only Mathlib and centers on principal ideals in commutative rings together with finite-set operations. The module introduces no new constants but records standard facts needed for later topological arguments.

proof idea

This is a definition-and-lemma module. The principal-ideal equality follows by direct expansion of the ideal membership predicate and the definition of divisibility. The remaining lemmas on finite operations and equality templates are one-line wrappers that apply ring axioms and set finiteness.

why it matters in Recognition Science

The module feeds the F6 topological capacity veto, supplying the ideal-equality step that lets linking invariants be well-defined only in three dimensions. It closes the algebraic foundation required by the Alexander-duality arguments in the downstream TopologicalVeto paper section.

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)