LogConsistency
The log-consistency predicate encodes the d'Alembert functional equation in logarithmic coordinates, requiring that G(t + u) + G(t - u) equals Q applied to the pair (G(t), G(u)) for all real t and u. Researchers deriving the uniqueness of the J-cost function from multiplicative consistency in Recognition Science cite this predicate when shifting from the positive reals to the additive group of reals. The declaration is a direct encoding of the equation with no lemmas or tactics involved.
claimFor functions $G : ℝ → ℝ$ and $Q : ℝ → ℝ → ℝ$, the predicate holds precisely when $G(t + u) + G(t - u) = Q(G(t), G(u))$ for all real numbers $t, u$.
background
The Full Unconditional module proves that any C² function F on positive reals obeying F(1) = 0, F(x) = F(1/x), and F(xy) + F(x/y) = P(F(x), F(y)) for some P must equal the J function with P the bilinear form 2uv + 2u + 2v. The auxiliary function G is the log reparametrization G(t) := F(exp t), which converts multiplicative consistency on ℝ₊ into an additive functional equation of d'Alembert type on ℝ. Upstream results include the definition of this reparametrization in the Cost.FunctionalEquation module as G(F)(t) = F(exp t) and the identification of the target solution G(t) = cosh(t) - 1 in the Gravity.JCostInflaton module.
proof idea
The declaration is a direct definition. It encodes the quantified equation without invoking lemmas or applying any tactics; the body consists solely of the forall statement over t and u.
why it matters in Recognition Science
This predicate is the conclusion of the theorem that derives log-coordinate consistency from multiplicative consistency of F. It forms a key step in the full unconditional proof that both F and P are forced to their explicit J and bilinear forms, completing the chain from normalization and symmetry assumptions. The step aligns with T5 J-uniqueness and the Recognition Composition Law in the framework.
scope and limits
- Does not assume any particular form for the function Q.
- Does not impose smoothness or normalization conditions on G.
- Does not establish existence or uniqueness of solutions.
- Does not reference physical constants or spatial dimensions.
formal statement (Lean)
150def LogConsistency (G : ℝ → ℝ) (Q : ℝ → ℝ → ℝ) : Prop :=
proof body
Definition body.
151 ∀ t u : ℝ, G (t + u) + G (t - u) = Q (G t) (G u)
152
153/-- From F-consistency to G-consistency in log coordinates. -/