Foundation Pinch Algebra

The pinch algebra toolkit

Foundation pinch algebra is a collection of formal results about divisibility and capacity. In mathematics, one number divides another if you can multiply the first by something to get the second. The central idea is mutual divisibility, where each of two numbers divides the other. In a commutative ring, a structure where addition and multiplication behave like the integers, this forces the two numbers to generate the same principal ideal. The framework's machine-checked library of formal theorems proves this as principal_ideal_eq_of_mutual_dvd: if a divides b and b divides a, then the ideal spanned by a equals the ideal spanned by b.

The name comes from the image of pinching two objects together until they coincide. The main theorem, imc_equality_template, packages this into a reusable template: given divisibility in both directions, conclude the principal ideals are equal. This is the algebraic heart of a later stage in the Birch and Swinnerton-Dyer program, where one side of an equality comes from Kato's work and the reverse divisibility comes from another source. The template turns two one-way statements into a two-way equality.

The second half of the module concerns operators and budgets. A function from a finite set onto an infinite set cannot exist; the theorem finite_not_onto_infinite states this as a formal obstruction. The related finite_operations_from_budget theorem says that with a positive cost per operation and a finite budget, only finitely many operations can be performed. These are the finite-capacity veto in its simplest form: a finite system cannot exhaust an infinite one.

In Recognition Science, these results serve as structural constraints. The framework models recognition as a discrete record of events with a forced cost, and pinch algebra provides the algebraic and set-theoretic limits that any such ledger must respect. The module does not derive the cost function or the golden ratio; it supplies the divisibility and capacity facts that later stages build upon. What a reader can take away is a precise sense of when two mathematical objects are interchangeable, and why finite resources impose hard ceilings on what a process can accomplish.

/-- **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⟩

/-- **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.3.2**: A function that is not surjective cannot map finite sets
    onto infinite sets. (Basic set-theoretic obstruction.)
    This is the finite-capacity veto in its simplest form. -/
theorem finite_not_onto_infinite {α β : Type*} (f : α → β)
    [Finite α] (hβ : Infinite β) : ¬Function.Surjective f := by
  intro hsurj
  have : Finite β := Finite.of_surjective f hsurj
  exact not_finite β

/-- **F5.3.1/3.2**: If the cost per operation is positive and the budget is finite,
    only finitely many operations can be performed. -/
theorem finite_operations_from_budget {n : ℕ} {cost budget : ℝ}
    (hcost : 0 < cost) (hbudget : 0 ≤ budget)
    (hfit : n * cost ≤ budget) :
    (n : ℝ) ≤ budget / cost := by
  rwa [le_div_iff₀ hcost]

What this page does not claim

This answer does not claim the module derives the cost function or the golden ratio. This answer does not claim the module proves the Birch and Swinnerton-Dyer conjecture itself. This answer does not claim the finite-capacity veto applies to infinite budgets.

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: