module module high

`IndisputableMonolith.NumberTheory.PrimeLedgerStructure`

The PrimeLedgerStructure module verifies that the J-cost satisfies the d'Alembert functional equation and records basic prime factorization facts for the Recognition ledger. Researchers building arithmetic extensions of J cite these results when constructing the prime cost spectrum. The arguments consist of direct algebraic checks against the definition of J together with imported properties from the Cost module.

claimThe module centers on the d'Alembert equation $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ together with the statement that every prime is irreducible in the positive integers under the J-cost structure.

background

The module imports the RS time quantum τ₀=1 tick from Constants and the J-cost function from the Cost module. It introduces the d'Alembert functional equation as the relation satisfied by J, which is defined via J(x)=(x+x^{-1})/2-1. The local theoretical setting prepares the extension of J from positive reals to natural numbers via prime factorization.

proof idea

This module collects lemmas that verify the d'Alembert equation for J, submultiplicativity, and prime irreducibility. Each lemma applies the functional equation definition and algebraic reduction using results imported from the Cost module.

why it matters in Recognition Science

The module supplies the d'Alembert verification and prime irreducibility facts imported by PrimeCostSpectrum to define the arithmetic cost c(n)=Σ v_p(n)·J(p). It supplies the bridge from the continuous J function to discrete number theory in the Recognition framework.

scope and limits

Does not prove the Recognition Composition Law for arbitrary real arguments.
Does not compute explicit J values on specific primes.
Does not define the full prime cost spectrum c(n).
Does not address zero or negative integers.

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