IndisputableMonolith.Foundation.DAlembert.Inevitability
Sets up cost functionals on the positive reals and polynomial route-combiners, then forces them under symmetry, normalization, and multiplicative consistency into a bilinear family. Recognition theorists cite it when deriving RCL from d'Alembert-style axioms without assuming the combiner form. The argument reduces P by symmetry and degree bounds, then pins the remaining coefficients.
claimA cost $F:\mathbb{R}_{>0}\to\mathbb{R}$ with a polynomial combiner $P$ that is symmetric, normalized, and multiplicatively consistent is forced into a bilinear family compatible with the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
background
Recognition Science derives physics from one functional equation, the Recognition Composition Law (RCL). The classical d'Alembert equation is the template: route-independence of a cost on positive reals forces an algebraic identity on a combiner $P(u,v)$. This module works in that setting.
Upstream, Cost supplies the native cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$), and Cost.Convexity proves strict convexity of both $J_{\log}(t)=\cosh t-1$ on $\mathbb{R}$ and $J$ on $\mathbb{R}_{>0}$, the foundation for uniqueness theorem T5. The module introduces a general cost functional $F$, symmetry and normalization predicates, a polynomial combiner $P$, and multiplicative consistency linking $F$ to $P$.
Sibling lemmas then relate symmetry of $F$ to symmetry of $P$, constrain $P$ by normalization, and reduce the admissible polynomial family.
proof idea
Definition layer first: cost functional, symmetry, normalization, polynomial combiner, and multiplicative consistency. Symmetry lemmas show that $P$-symmetry implies $F$-swap and $F$-symmetry identities, and conversely that $F$-symmetry recovers $P$-symmetry. Normalization plus symmetry constrain the low-degree terms of $P$. A degree argument forces the polynomial form; a further reduction collapses the admissible family to a bilinear ansatz. The terminal lemma forces that bilinear family (coefficients pinned up to the RCL normal form).
why it matters in Recognition Science
This is the local inevitability engine for the d'Alembert branch of the foundation. Downstream, FullUnconditional imports it to prove the strongest RCL inevitability: both $F$ and $P$ forced with no a-priori assumption on $P$. RightAffineFromFactorization uses the same constraints when closing Gap 4 (factorization gate forces the RCL polynomial $2uv+2u+2v$). GeneralizedDAlembert relaxes the polynomial-degree hypothesis via continuity, building on the forced bilinear skeleton. LogicAsFunctionalEquation and PolynomialityFromLogic treat logic itself as a functional equation and recover polynomiality; they sit on this module's definitions and forcing lemmas. In the global chain this supports T5 (J-uniqueness) and the RCL landmark.
scope and limits
- Does not prove full unconditional RCL inevitability; that lives in FullUnconditional.
- Does not discharge continuity-only regularity; GeneralizedDAlembert handles that relaxation.
- Does not alone force right-affinity from factorization gates.
- Does not derive physical constants, mass ladder, or dimensional forcing (T6–T8).
- Does not claim uniqueness of J without the convexity and normalization package from Cost.
used by (5)
depends on (2)
declarations in this module (13)
-
structure
CostFunctional -
def
IsSymmetric -
def
IsNormalized -
structure
PolynomialCombiner -
def
HasMultiplicativeConsistency -
theorem
F_div_swap_of_P_symmetric -
theorem
F_symmetric_of_P_symmetric -
theorem
symmetry_and_normalization_constrain_P -
theorem
P_symmetric_from_F_symmetric -
theorem
polynomial_form_forced -
theorem
bilinear_family_reduction -
theorem
bilinear_family_forced -
theorem
axiom_bundle_necessary