Foundation Generalized Dalembert Continuous Combiner Bilinear Classification

The continuous combiner theorem

The recognition framework, a discrete record of events and their costs, treats comparison as a bookkeeping operation. A combiner is the rule that merges two costs into one. The theorem continuous_combiner_bilinear_classification states that if a combiner is continuous and satisfies the framework's laws of logic, then it must take the bilinear form P(u, v) = 2u + 2v + c·u·v for some constant c. This means the combined cost is a simple arithmetic expression: twice each input, plus a product term scaled by c.

The result rests on a classical classification theorem. The d'Alembert functional equation H(x+y) + H(x−y) = 2H(x)H(y), studied since the 18th century, has exactly three continuous solutions with H(0) = 1: the constant 1, a hyperbolic cosine cosh(αx), or a trigonometric cosine cos(αx). The framework proves this classification internally as aczel_kannappan_continuous_dAlembert, then uses it to force the bilinear form. The proof chain upgrades continuity to smoothness via a mollifier construction, derives a second-order differential equation, and applies ODE uniqueness in each branch of the trichotomy on H''(0).

The theorem does not claim that continuity alone suffices. The framework's own counterexample, the quartic log-cost, shows that a continuous combiner can fail the required second-derivative identity. The theorem therefore requires three additional inputs beyond continuity: finite smoothness of the cost function, a second-derivative identity, and an affine completion condition. These are packaged in the structure ContinuousCombinerAnalysisInputs. Without them, the bilinear conclusion does not follow.

What the theorem establishes is a sharpening of an earlier result. The previous Translation Theorem required the combiner to be a polynomial of total degree at most two. This new theorem replaces that polynomial restriction with continuity plus the three analytic inputs. The polynomial case becomes a special instance, subsumed by the continuous version. The framework's library proves this subsumption in laws_continuous_subsumes_polynomial.

Within the framework, this result matters because it narrows the possible forms of comparison. The bilinear form is the only shape a continuous, law-abiding combiner can take, once the analytic inputs hold. The constant c is not fixed by this theorem; it remains a free parameter. The framework's later forcing chain, which derives specific values for physical constants, depends on additional structure beyond this classification.

/-- **Continuous-combiner bilinear classification** (hypothesis-package form).

The final bilinear conclusion follows if the explicit analysis package is
provided. It is not automatic from `SatisfiesLawsOfLogicContinuous`; the
quartic log-cost refutes the proposed second-derivative input. -/
theorem continuous_combiner_bilinear_classification
    (C : ComparisonOperator)
    (h : SatisfiesLawsOfLogicContinuous C)
    (hInputs : ContinuousCombinerAnalysisInputs C h) :
    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
      (∀ x y : ℝ, 0 < x → 0 < y →
        derivedCost C (x * y) + derivedCost C (x / y)
          = P (derivedCost C x) (derivedCost C y)) ∧
      (∀ u v, P u v = 2*u + 2*v + c*u*v) := by
  have hSmooth := continuous_combiner_log_smoothness_bootstrap C h hInputs.finite_smoothness
  have hLog := continuous_combiner_psi_affine_forcing C h hSmooth
    hInputs.second_derivative hInputs.psi_affine
  exact log_bilinear_positive_cost_bilinear (derivedCost C) hLog

/-- **Aczél–Kannappan classification** (proved theorem, not axiom):
every continuous solution of the d'Alembert functional equation
`H(x+y) + H(x-y) = 2 H(x) H(y)` with `H(0) = 1` is either the
constant 1, a hyperbolic cosine, or a trigonometric cosine.

The proof reduces to
`IndisputableMonolith.Cost.FunctionalEquation.dAlembert_classification`,
which assembles the integration bootstrap, universal-coefficient ODE
derivation, and ODE uniqueness lemmas into the disjunction. -/
theorem aczel_kannappan_continuous_dAlembert
    (H : ℝ → ℝ) (hCont : Continuous H) (h_one : H 0 = 1)
    (hEq : ∀ x y : ℝ, H (x + y) + H (x - y) = 2 * H x * H y) :
    (∀ x, H x = 1) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cos (α * x)) :=
  IndisputableMonolith.Cost.FunctionalEquation.dAlembert_classification
    H h_one hCont hEq

/-- Explicit package of the extra analysis needed to force bilinearity from
an arbitrary continuous combiner. This is deliberately a hypothesis package,
not an axiom. The quartic-log obstruction shows the package is not automatic
from `SatisfiesLawsOfLogicContinuous`. -/
structure ContinuousCombinerAnalysisInputs
    (C : ComparisonOperator)
    (h : SatisfiesLawsOfLogicContinuous C) : Prop where
  finite_smoothness : ContinuousCombinerMollifierFiniteSmoothness C h
  second_derivative :
    ContinuousCombinerSecondDerivativeInput C h
      (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
  psi_affine :
    ContinuousCombinerPsiAffineCompletion C h
      (continuous_combiner_log_smoothness_bootstrap C h finite_smoothness)
      second_derivative

/-- Every polynomial-LoL operator is a continuous-LoL operator. The bilinear
conclusion still requires the explicit analysis package at this level; the
ordinary polynomial theorem in `LogicAsFunctionalEquation` remains the
unconditional route. -/
theorem laws_continuous_subsumes_polynomial
    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C)
    (hInputs : ContinuousCombinerAnalysisInputs C
      (laws_polynomial_implies_continuous C h)) :
    ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
      (∀ x y : ℝ, 0 < x → 0 < y →
        derivedCost C (x * y) + derivedCost C (x / y)
          = P (derivedCost C x) (derivedCost C y)) ∧
      (∀ u v, P u v = 2*u + 2*v + c*u*v) :=
  RCL_is_unique_functional_form_of_logic_continuous C
    (laws_polynomial_implies_continuous C h) hInputs

What this page does not claim

Continuity alone forces the bilinear form without the three analytic inputs. The constant c is determined by this theorem. The bilinear classification applies to non-continuous combiners.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/GeneralizedDAlembert.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: