IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCMonotoneDAlembert
Completeness-free regularity for the Recognition cost: a monotone additive real map is linear, and a monotone even normalized d'Alembert solution is cosh composed with a linear map. Replaces the ContinuousOn hypothesis in classical J-uniqueness by pure order theory on an Archimedean field. Downstream native-cost uniqueness imports this brick. The argument chains Cauchy linearity via rational density into the d'Alembert reduction of the RCL.
claimOn an Archimedean ordered field, every monotone $f$ with $f(x+y)=f(x)+f(y)$ satisfies $f(x)=f(1)\cdot x$. Consequently every even, normalized, monotone solution of d'Alembert's equation $h(s+t)+h(s-t)=2h(s)h(t)$ is of the form $h=\cosh\circ L$ with $L$ additive and linear. Under the real cost hypotheses plus monotonicity on positives, the Recognition Composition Law forces the cost into the $\cosh\circ\log$ (equivalently $J$) scale family.
background
Classical T5 J-uniqueness (law_of_logic_forces_jcost) takes ContinuousOn as analytic input and therefore presupposes the continuum. Section 9 asks whether that input can be swapped for a purely order-theoretic hypothesis available on any Archimedean ordered field, without least-upper-bound completeness. This module answers yes at the additive layer the RCL reduction lands on.
The reduction is standard: set $g=F+1$, $h(t)=g(e^t)$; the Recognition Composition Law becomes d'Alembert's functional equation $h(s+t)+h(s-t)=2h(s)h(t)$ with even $h$. Solutions of that shape are $\cosh$ composed with an additive map. The remaining regularity question is whether a monotone such $h$ forces the inner additive map to be linear.
Upstream material lives in Cost and Cost.FunctionalEquation (T5 functional-equation helpers). The module never invokes completeness: the only density fact used is existence of a rational between any two reals in an Archimedean field.
proof idea
The load-bearing step is Cauchy linearity under monotonicity: monotone_additive_isLinear (and the nonnegative variant) prove $f(x)=f(1)\cdot x$ by the usual rational homogeneity plus sandwiching via exists_rat_btwn, with no LUB.
Around that core the module builds d'Alembert calculus under monotonicity: duplication, product and difference-square identities, comparison lemmas (dAlembert_ge_one_of_monotone, dAlembert_diff_eq_of_monotone), and additive forms for $h$ and the companion $S$. Multiplicativity of the phase (phi_mul_of_monotone) feeds dAlembert_cosh_of_monotone: even, normalized, monotone d'Alembert solutions are $\cosh\circ$ linear. The capstone composition_law_monotone_forces_cosh_family assembles these into the cost-scale conclusion from RCL plus MonotoneOn.
why it matters in Recognition Science
This is the §9 regularity-substitute brick for completeness-free cost forcing. It dissolves the continuum posit on the cost side: monotonicity replaces continuity, so the framework's arbitrary analytic content drops to one unit of scale (faithfulness of the scale family is handled downstream).
Parent consumer is PRCNativeCostUniqueness, which imports this module to obtain native cost uniqueness from the monotone d'Alembert package (dAlembert_cosh_of_monotone and the composition-law forcing theorem). In the forcing chain this underwrites T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$) without ContinuousOn, keeping the RCL route intact on any Archimedean ordered field.
With the assembly closed in the positive direction, the open §9 question is answered: order-theoretic regularity suffices at the additive layer the RCL reduction produces.
scope and limits
- Does not prove J-uniqueness alone; supplies the monotone regularity brick consumed downstream.
- Does not use or claim least-upper-bound completeness; only Archimedean rational density.
- Does not treat non-monotone additive (pathological Hamel) solutions.
- Does not fix the overall cost scale; faithfulness of the scale family is separate.
- Does not address discrete or non-Archimedean base fields.
used by (1)
depends on (2)
declarations in this module (18)
-
theorem
monotone_additive_isLinear -
theorem
monotone_additive_nonneg_isLinear -
theorem
dAlembert_duplication -
theorem
dAlembert_ge_one_of_monotone -
theorem
dAlembert_prod -
theorem
dAlembert_diff_sq -
theorem
dAlembert_diff_eq_of_monotone -
theorem
dAlembert_add_of_monotone -
theorem
dAlembert_S_add_of_monotone -
theorem
phi_mul_of_monotone -
theorem
dAlembert_cosh_of_monotone -
theorem
composition_law_monotone_forces_cosh_family -
theorem
cosh_scale_curvature -
theorem
H_jcost_eq_cosh -
theorem
cosh_mul_monotoneOn -
theorem
about -
theorem
H_jcost_monotoneOn -
theorem
jcost_forced_by_order