pith. sign in
module module high

IndisputableMonolith.Mathematics.GoldbachFromRS

show as:
view Lean formalization →

The GoldbachFromRS module models primes as recognition equilibria under the J-cost function to derive even-number decompositions into prime pairs. Researchers connecting number theory to the Recognition Science framework would cite it for its structural definitions. The module organizes the argument via gap categories, symmetric pair costs, and explicit certificates without containing any proofs.

claimPrimes $p$ satisfy the equilibrium condition $J(p) = 0$ where $J(x) = (x + x^{-1})/2 - 1$, with unit cost at $p=1$. Even integers are certified as sums of such prime pairs via symmetric cost-zero representations.

background

The module imports the Cost module, which supplies the J-cost function measuring deviation from recognition equilibrium. In this setting J(1) = 0 defines unit cost, and primes are equilibria where J(p) = 0. The module introduces PrimeGapCategory to classify gaps, primeGapCategoryCount to enumerate them, prime_unit_cost and prime_pair_symmetric to assign costs to pairs, and GoldbachRSCert together with goldbachRSCert to certify decompositions.

proof idea

This is a definition module, no proofs. It declares the six sibling objects that structure the Goldbach derivation: gap categories, their counts, unit costs for primes, symmetric pair predicates, and the certificate type with its constructor.

why it matters in Recognition Science

The module supplies the definitions needed to embed the classical Goldbach statement inside Recognition Science equilibria. It feeds downstream results that treat Goldbach representations as consequences of the forcing chain and RCL. The GoldbachRSCert object directly encodes the zero-cost prime-pair condition that links to the phi-ladder mass formula and eight-tick octave.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)