module module high

`IndisputableMonolith.NumberTheory.PrimeLedgerStructure`

The module establishes the d'Alembert functional equation for the Recognition Science cost function J and supplies basic prime factorization lemmas. Researchers building the prime cost spectrum cite it to extend J multiplicatively over natural numbers. The argument consists of algebraic verifications that J obeys the composition law together with direct checks of prime irreducibility.

claimThe d'Alembert functional equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ holds for the RS cost $J$, with auxiliary results that every prime is irreducible and every integer greater than 1 has a prime factor.

background

The module sits in the NumberTheory domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the cost function J from Cost. J is defined by J(x) = (x + x^{-1})/2 - 1, equivalently cosh(log x) - 1. The central object is the d'Alembert equation, which is the Recognition Composition Law specialized to this J.

proof idea

The module contains a collection of lemmas. Direct substitution of the hyperbolic definition of J into the target equation yields the identity after algebraic rearrangement; separate lemmas then verify that primes remain irreducible under the induced cost ordering and that every integer factors into primes.

why it matters in Recognition Science

This module supplies the arithmetic scaffolding required by PrimeCostSpectrum, which defines the integer cost c(n) = Σ v_p(n) J(p). It thereby connects the real-valued J to the discrete prime ledger used for mass formulas and the phi-ladder in the Recognition Science framework.

scope and limits

Does not derive the explicit form of J from the forcing chain.
Does not compute numerical values of c(n) for specific integers.
Does not prove the fundamental theorem of arithmetic in full.
Does not address composite cost spectra beyond prime factorization.

used by (1)

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

IndisputableMonolith.NumberTheory.PrimeCostSpectrum module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (15)

def SatisfiesDAlembert L56
theorem cosh_satisfies_dalembert L60
theorem rs_cost_satisfies_dalembert L67
theorem cosh_no_real_zeros L75
theorem cosh_at_zero L81
theorem jcost_log_zero_unique L86
theorem primes_are_irreducible L100
theorem has_prime_factor L113
theorem j_dalembert L125
theorem j_submult L132
theorem j_functional_equation L155
theorem inversion_fixed_point L160
theorem j_zero_at_fixed_point L173
theorem j_positive_off_fixed_point L176
theorem structural_parallel_certificate L227