Cost Functional Equation Strict

The strict form

A functional equation is a rule that a function must obey, and the cost functional equation is the specific rule that governs the price of recognition in this framework. The strict variant is a tightened version of that rule. Where the main theorem asks for five separate conditions, the strict form shows that only two of them actually do the work: the composition law and a limit-form calibration. The other three conditions, reciprocity, normalization, and the ordinary calibration, turn out to be consequences of those two, not independent requirements.

The composition law is the heart of the matter. It says that the cost of recognizing a combined event must be forced by the costs of recognizing its parts, in a way that cannot be chosen freely. The limit-form calibration is a technical condition that supplies the smoothness the classical argument needs. Together they force the cost function to be exactly J(x) = (x + 1/x)/2 - 1 for every positive x. This is not an approximation and not a fitted curve; it is a proved equality.

This result has a history worth knowing. Until July 2026, the strict theorem was vacuous, meaning its premise was impossible to satisfy, so the statement proved nothing at all. The limit-form calibration was written on the wrong kind of neighborhood, which made it false at the point where it mattered. The fix was to puncture that neighborhood and add a witness that the condition actually has content. After that fix, the theorem stands on its own two premises, with no hidden assumptions and no extra machinery.

What this establishes in plain language is that the entire cost structure of the framework rests on a single forced relationship. If you accept that recognition costs obey a composition law and a mild smoothness condition, you get the exact form of the cost function for free. The strict result is the cleanest statement of that fact, and it is the version the framework's library points to when someone asks for the sharpest result.

/-- **The cost theorem on two premises, unconditionally.**

`composition_logCurvature_forces_jcost` is stated in `FunctionalEquation`, which
does not import the module that builds the `AczelSmoothnessPackage` instance, so
there it carries the package as an instance argument. This module does import it,
so here the theorem stands with no instance argument and no hypotheses beyond the
composition law and unit log curvature. Cite this one. -/
theorem composition_logCurvature_forces_jcost_unconditional (F : ℝ → ℝ)
    (hComp : SatisfiesCompositionLaw F)
    (hκ : HasLogCurvature (H F) 1) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
  composition_logCurvature_forces_jcost F hComp hκ

/-- **The cost theorem on two premises, unconditionally.**

`composition_logCurvature_forces_jcost` is stated in `FunctionalEquation`, which
does not import the module that builds the `AczelSmoothnessPackage` instance, so
there it carries the package as an instance argument. This module does import it,
so here the theorem stands with no instance argument and no hypotheses beyond the
composition law and unit log curvature. Cite this one. -/
theorem composition_logCurvature_forces_jcost_unconditional (F : ℝ → ℝ)
    (hComp : SatisfiesCompositionLaw F)
    (hκ : HasLogCurvature (H F) 1) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
  composition_logCurvature_forces_jcost F hComp hκ

/-- Limit-form log calibration supplies the continuity needed by the Aczél
d'Alembert route, so the explicit `ContinuousOn F (Set.Ioi 0)` premise can be
removed from this T5 variant.

Only `hComp` and `hLogCalib` are used: the other three premises are consequences
of that pair. They are retained so existing callers keep type-checking. -/
theorem law_of_logic_forces_jcost_of_log_calibration (F : ℝ → ℝ)
    [AczelSmoothnessPackage]
    (_hRecip : IsReciprocalCost F)
    (_hNorm : IsNormalized F)
    (hComp : SatisfiesCompositionLaw F)
    (_hCalib : IsCalibrated F)
    (hLogCalib : IsCalibratedLimit F) :
    ∀ x : ℝ, 0 < x → F x = Cost.Jcost x :=
  composition_logCurvature_forces_jcost F hComp hLogCalib

What this page does not claim

This page does not claim that the strict theorem is the only route to the cost function; the five-premise version still exists. This page does not claim that the composition law alone forces the cost function; the limit-form calibration is also required. This page does not claim that the strict result proves anything about the physical interpretation of the cost function; it only establishes the mathematical equality.

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/Cost/FunctionalEquationStrict.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: