IndisputableMonolith.NumberTheory.PrimeLedgerStructure
Module PrimeLedgerStructure develops the d'Alembert functional equation and supporting properties for the Recognition Science J-cost on positive reals, plus basic prime factorization facts. Researchers extending J to arithmetic functions on naturals cite these results when building the prime cost spectrum. The module assembles independent lemmas on equation satisfaction, uniqueness, and irreducibility rather than a single chained proof.
claimThe d'Alembert functional equation for the cost function is $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, where $J(x) = (x + x^{-1})/2 - 1$. Related statements include that $J$ is submultiplicative, has a unique zero at $x=1$, and that primes are irreducible in the associated ledger structure.
background
The module imports the RS-native time quantum from Constants, where τ₀ equals one tick, and the cost function J from the Cost module. It works in the setting where J derives from the forcing chain and satisfies the Recognition Composition Law. Sibling results introduce the predicate SatisfiesDAlembert, prove that cosh(log x) satisfies the equation, establish that the RS cost J satisfies it, and record that J has no real zeros except at the fixed point.
proof idea
The module collects separate lemmas rather than a single proof. One lemma shows cosh satisfies d'Alembert by direct substitution. Another transfers the property to the RS cost J via its definition as cosh(log x) minus one. Additional lemmas establish log-zero uniqueness for J, submultiplicativity, and that every natural number greater than one has a prime factor with primes irreducible.
why it matters in Recognition Science
This module supplies the functional-equation foundation required by the downstream PrimeCostSpectrum module, which defines the arithmetic extension c(n) as the sum over prime powers of v_p(n) times J(p). It fills the d'Alembert component of the Recognition Composition Law and supports the transition from continuous J to discrete prime-ledger arithmetic. The results sit between the core Cost definitions and the number-theoretic spectrum used for mass and coupling calculations.
scope and limits
- Does not derive numerical values for constants such as alpha inverse.
- Does not address the eight-tick octave or spatial dimension forcing.
- Does not connect J to the phi-ladder mass formula.
- Does not prove the full Recognition Composition Law beyond d'Alembert form.
used by (1)
depends on (2)
declarations in this module (15)
-
def
SatisfiesDAlembert -
theorem
cosh_satisfies_dalembert -
theorem
rs_cost_satisfies_dalembert -
theorem
cosh_no_real_zeros -
theorem
cosh_at_zero -
theorem
jcost_log_zero_unique -
theorem
primes_are_irreducible -
theorem
has_prime_factor -
theorem
j_dalembert -
theorem
j_submult -
theorem
j_functional_equation -
theorem
inversion_fixed_point -
theorem
j_zero_at_fixed_point -
theorem
j_positive_off_fixed_point -
theorem
structural_parallel_certificate