IndisputableMonolith.Foundation.PinchAlgebra
PinchAlgebra module supplies lemmas on principal ideals and finiteness in commutative rings to support the Recognition Science foundation layer. TopologicalVeto cites these for algebraic prerequisites in the D=3 capacity veto. Each lemma follows from direct application of Mathlib ring axioms and set finiteness properties.
claimIn a commutative ring, the principal ideals satisfy $(a)=(b)$ if and only if $a$ divides $b$ and $b$ divides $a$.
background
The module imports Mathlib and collects short lemmas under the F5.1.2/1.4 heading on principal ideal equality from mutual divisibility. Sibling results cover equality templates, the fact that finite sets are not onto infinite ones, and operations constrained by a budget. These establish basic algebraic identities in commutative rings for use in later foundation constructions.
No deeper structures such as the J-cost function or phi-ladder appear here; the setting remains standard ring theory.
proof idea
This module contains multiple independent short lemmas; each applies standard divisibility and finiteness facts from Mathlib without a single overarching argument.
why it matters in Recognition Science
Results feed the TopologicalVeto module for the F6 topological capacity veto in D=3, specifically supporting linking_only_in_D3. The module closes algebraic prerequisites listed under F5.1.2/1.4 in the foundation paper.
scope and limits
- Does not treat non-commutative rings.
- Does not reference the J-function or Recognition Composition Law.
- Does not derive the eight-tick octave or spatial dimension D=3.
- Does not bound the fine-structure constant alpha.