pith. machine review for the scientific record. sign in
def definition def or abbrev high

LogBilinearIdentity

show as:
view Lean formalization →

LogBilinearIdentity defines the property that a real-valued function G obeys the bilinear functional equation G(t+u) + G(t-u) = 2G(t) + 2G(u) + c G(t)G(u) for all real t and u. Analysts classifying continuous log-costs or lifting combiners in the Recognition Science pipeline cite this definition when assembling the algebraic core after smoothness analysis. The declaration is introduced as a direct definition of the equation with no lemmas or tactics applied.

claimA map $G : ℝ → ℝ$ and scalar $c ∈ ℝ$ obey the log-bilinear identity when $G(t+u) + G(t-u) = 2G(t) + 2G(u) + c · G(t) · G(u)$ holds for every pair of real numbers $t, u$.

background

The GeneralizedDAlembert module develops the continuous-combiner version of the laws of logic by relaxing the polynomial-degree bound on the route-independence combiner. It reparametrizes the cost function F to logarithmic coordinates via the map G(t) := F(e^t), converting multiplicative structure into additive form. The log-bilinear identity then encodes the resulting functional equation with a possible quadratic term scaled by c.

proof idea

The declaration is introduced as a direct definition of the bilinear equation in log coordinates. No lemmas are invoked; the body simply unfolds the universal quantification over t and u.

why it matters in Recognition Science

This definition supplies the algebraic target for the classified log-cost bilinear theorem, which proves every classified log-cost satisfies the identity for some c. It also enables the affine lift to the standard d'Alembert equation via H(t) = 1 + (c/2)G(t), as used in the log-bilinear affine lift theorems and the positive-cost bilinear assembly. Within the Recognition framework it completes the continuous-combiner pipeline, replacing the polynomial hypothesis in the Translation Theorem with the Aczél–Kannappan trichotomy.

scope and limits

formal statement (Lean)

 322def LogBilinearIdentity (G : ℝ → ℝ) (c : ℝ) : Prop :=

proof body

Definition body.

 323  ∀ t u : ℝ,
 324    G (t + u) + G (t - u) = 2 * G t + 2 * G u + c * G t * G u
 325
 326/-- A classified log-coordinate cost: parabolic, hyperbolic, trigonometric,
 327or zero. This is the algebraic target left after the smoothness/affine-forcing
 328analysis has been done. -/

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.