IndisputableMonolith.Foundation.DAlembert.FullUnconditional
Module that closes the unconditional path from multiplicative cost consistency to d'Alembert and the forced cosh form of the cost, with no free ansatz on the pairing P. Foundation readers cite it for the T5-facing argument that RCL and J-uniqueness follow once F is fixed by symmetry, normalization, and smoothness. It computes P from F, proves reciprocal symmetry of P, and packages cosh-forcing and RCL-form results as theorems or named hypotheses.
claimIf a cost $F:\mathbb{R}_{+}\to\mathbb{R}$ is multiplicatively consistent, the induced pairing $P$ obeys d'Alembert's functional equation. Reciprocal symmetry of $F$ forces symmetry of $P$. Even continuous solutions force $F$ (equivalently the J-cost) into the shape $\cosh\circ\log-1$, yielding the Recognition Composition Law form with no a-priori assumption on $P$.
background
Recognition Science fixes the cost functional by a uniqueness theorem (T5): the J-cost is $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$. The Recognition Composition Law (RCL) is the two-argument identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Multiplicative consistency of a cost $F$ on positive reals induces a pairing $P$ that must satisfy a d'Alembert-type equation; the question is whether that equation, and the cosh solution, are forced or merely chosen.
Upstream, DAlembert.Inevitability shows d'Alembert is the unique form compatible with multiplicative consistency of a cost. DAlembert.Unconditional strengthens this: once $F$ is fixed by symmetry, normalization, calibration, and smoothness, $P$ is computed from the functional equation rather than assumed. Cost-layer helpers supply the T5 functional-equation lemmas and the optional Aczél closure path.
This module sits on top of those imports and develops the full unconditional surface: symmetry of $P$ from reciprocal symmetry of $F$, diagonal and zero-endpoint evaluations, log-consistency bridges, the map from RCL-style $G$ to a d'Alembert $H$, and the cosh-forcing and RCL-form statements.
proof idea
Not a single theorem: a structured development. First block derives symmetry and boundary facts for $P$ from reciprocal symmetry of $F$ (symmetry on the range, values at zero from each side, diagonal restriction). A log-consistency layer converts multiplicative consistency into an additive d'Alembert problem on the log coordinate. From an RCL-shaped generator one obtains a d'Alembert $H$; even solutions are isolated. The module then states the cosh-forcing claim both as a named hypothesis interface and as a theorem form, and likewise packages the claim that consistency forces the RCL algebraic shape. Argument style is reduction to the unconditional and inevitability cores, plus Cost functional-equation lemmas, rather than a fresh analytic existence proof.
why it matters in Recognition Science
Closes the foundation gap between "d'Alembert is inevitable for consistent costs" and "the cost must be the T5 J-cost / cosh form, and the composition law must be RCL," without smuggling an assumption on $P$. That is the strongest RCL-inevitability surface the stack currently exposes, and it is what a T5 uniqueness argument wants as input: $P$ is an output of $F$, not a modeling choice.
Downstream edges are empty in the graph snapshot, so this module is a terminal assembly point in the DAlembert cluster rather than a leaf lemma inside a larger proof. It still feeds the forcing chain narrative at T5 (J-uniqueness) and the RCL landmark in the primer. Sibling names mark the live load-bearing pieces: cosh-forcing as theorem versus hypothesis, and consistency-forces-RCL-form as hypothesis interface, so auditors can see exactly where the argument is fully discharged versus still named.
scope and limits
- Does not by itself re-prove T5 J-uniqueness from raw axioms; it assembles the d'Alembert and RCL bridge.
- Does not remove every hypothesis interface: cosh-forcing and RCL-form still appear as named hypothesis objects alongside theorem forms.
- Does not treat discrete eight-tick, $D=3$, or constants ($c$, $\hbar$, $G$, $\alpha$); scope is cost functional equations only.
- Does not claim Aczél-free status for every corollary; Aczél closure remains an optional imported compatibility path.
- Does not supply downstream consumers in the current graph; used_by is empty.
depends on (5)
declarations in this module (18)
-
theorem
P_symmetric_of_F_symmetric -
theorem
P_symmetric_on_range -
theorem
P_at_zero_left -
theorem
P_at_zero_right -
theorem
P_diagonal -
def
LogConsistency -
theorem
log_consistency_of_mult_consistency -
theorem
H_dAlembert_of_G_RCL -
theorem
dAlembert_even_solution -
def
dAlembert_forces_cosh_hypothesis -
theorem
dAlembert_forces_cosh_is_theorem -
def
consistency_forces_RCL_form_hypothesis -
theorem
consistency_forces_RCL_form_is_theorem -
structure
FullUnconditionalHypotheses -
theorem
full_unconditional_inevitability -
theorem
full_inevitability_explicit -
theorem
washburn_full_unconditional -
theorem
consistency_forces_RCL_polynomial