about
plain-language theorem explainer
Non-vacuity witness that the monotone d'Alembert development is not hanging on an empty hypothesis class: the chain that forces the cosh family under `MonotoneOn` is inhabited. Anyone citing the PRC monotone route to the Recognition Composition Law / J-uniqueness path needs this to know the ambient class is real. Extraction gives no proof body; the role is structural, not computational.
Claim. The hypothesis class on which the monotone d'Alembert chain rests (monotonicity on the relevant domain) is non-empty: there exists at least one witness so the subsequent forcing results are not vacuous implications from False.
background
Module PRCMonotoneDAlembert develops the classical d'Alembert functional equation under monotonicity, inside Primitive Recognition Calculus. Sibling results treat additive monotone maps as linear, duplication and product identities, difference-square formulae, and the passage from monotone d'Alembert solutions to a cosh family, ending at the composition-law statement that monotone solutions are forced into the cosh shape.
In Recognition Science that shape is the J-cost: $J(x)=\cosh(\log x)-1=(x+x^{-1})/2-1$, the unique solution singled out in the forcing chain (T5) and tied to the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Monotonicity is the regularity that keeps the classification from admitting wild solutions.
Upstream cost and functional-equation material supplies the algebraic identities; the present declaration only certifies that the monotone hypothesis class the rest of the file quantifies over is inhabited.
proof idea
No proof body is present in the extract (zero body lines, status other). Role is that of a non-vacuity / inhabitation witness for the MonotoneOn hypothesis class used by the sibling lemmas (dAlembert_ge_one_of_monotone, dAlembert_diff_eq_of_monotone, dAlembert_cosh_of_monotone, composition_law_monotone_forces_cosh_family, etc.). Expect a one-line existence term or a trivial inhabitant of the monotone class rather than a multi-step tactic script.
why it matters
Without a non-vacuity witness, every theorem of the form "monotone d'Alembert solutions are cosh" is formally true if the premise class is empty. This declaration closes that gap for the PRC monotone route into J-uniqueness (forcing T5) and the Recognition Composition Law.
Downstream, the cosh/J identification feeds constants and cosmology layers that quote $\phi$-ladder scales and $\alpha$ bounds; the monotone classification is part of why those layers may treat $J$ as forced rather than stipulated. Among siblings, it underwrites composition_law_monotone_forces_cosh_family, the local capstone.
It does not itself derive $\phi$, the eight-tick octave, or $D=3$; those sit later in the forcing chain (T6–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.