Cost Uniqueness

The role of the zero derivative

The uniqueness proof for the cost function J(x) = (x + 1/x)/2 - 1 depends on a specific initial condition: after a change of variables into log coordinates, the function H(t) = F(e^t) + 1 must have derivative zero at t = 0. This condition, deriv H 0 = 0, is not one of the five stated axioms. It is a consequence of the reciprocal symmetry axiom, which forces the transformed function to be even, and an even function that is differentiable at zero must have zero derivative there.

If even_deriv_at_zero were false or dropped, the composition law would still force H to satisfy the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u). The general continuous solutions to that equation are H(t) = cosh(κ t) for a real parameter κ, together with the degenerate case H(t) = 0. The log-curvature calibration condition, which fixes the second derivative at zero to be 1, would then force κ = 1, giving H(t) = cosh(t) and hence the unique cost. But without the zero-derivative condition, the calibration alone does not select cosh: the family cosh(κ t) with κ ≠ 1 also satisfies the composition law and the same normalization H(0) = 1, and each would produce a different cost function.

The theorem law_of_logic_forces_jcost states that the five axioms together force J. The proof of that theorem relies on the d'Alembert solution theorem, which takes deriv H 0 = 0 as an explicit hypothesis. If that hypothesis were dropped, the conclusion would fail: the axioms would no longer single out one cost function. The reciprocal symmetry axiom is what supplies the zero derivative, so dropping even_deriv_at_zero is not a separate weakening; it is the same as dropping reciprocal symmetry. The uniqueness story therefore rests on the fact that looking both ways is free, and that fact is what kills the extra parameter in the cosh family.

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_cosh_solution · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM reciprocal_implies_G_even · IndisputableMonolith/Cost/FunctionalEquation.lean

The differentiability hypothesis

The uniqueness theorem forces the cost function to be J(x) = (x + 1/x)/2 - 1 from five conditions. One of those conditions is continuity. The proof needs more than continuity to reach the differential equation whose solution is cosh. It needs a second derivative. The gap between the two is bridged by a package of regularity hypotheses drawn from Aczél theory.

cosh_satisfies_differentiable is one of those hypotheses. It states that the hyperbolic cosine satisfies the differentiability condition required by the regularity package. In the formal proof this declaration is a small lemma, one of three that verify the package for cosh. The other two cover continuity and the bootstrap from differentiability to smoothness. Together they confirm that the candidate solution passes through the same regularity machinery that the uniqueness theorem uses.

The declaration contributes to the proof of dAlembert_cosh_solution_of_log_curvature, which derives cosh from the d'Alembert equation plus a log-curvature calibration. That theorem in turn feeds the main uniqueness result. Without these regularity checks the derivation would stop at continuity and never reach the second derivative that selects cosh. The declaration is therefore not a separate result about cost; it is a supporting lemma that keeps the proof of the main theorem honest.

For the cost-uniqueness page the declaration belongs in the apparatus, not in the lead. The page teaches that five conditions force one cost function. The regularity package is an internal detail of how the proof crosses from continuity to differentiability. A reader who wants the full chain can follow the machine-checked anchors. A reader who wants the idea can stop at the five conditions and the conclusion.

THEOREM cosh_satisfies_differentiable · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_cosh_solution_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

The addition law

Recognition costs obey a forced composition rule: the cost of recognizing a product of two ratios plus the cost of recognizing their quotient equals a fixed expression in the two individual costs. The theorem composition_law_equiv_coshAdd proves this rule is equivalent to a statement about the cost in log coordinates, where the ratio x becomes the shift t = log x. In those coordinates the cost function G satisfies DirectCoshAdd: for any two shifts t and u, G(t+u) + G(t-u) equals 2 times G(t) times G(u) plus 2 times G(t) plus 2 times G(u).

The plain meaning is that the composition law, which looks like a rule about multiplying and dividing ratios, is really a rule about adding and subtracting shifts. Multiplication of positive ratios becomes addition of real shifts under the logarithm, and the composition law becomes an addition identity for the cost in that coordinate. The definition DirectCoshAdd states this identity directly, without mentioning ratios at all.

The identity earns its name because the unique cost function J(x) = (x + 1/x)/2 - 1 satisfies it. In log coordinates that cost is cosh(t) - 1, and the theorem Jcost_cosh_add_identity verifies the addition identity for that function. The theorem composition_logCurvature_forces_jcost then shows that the composition law together with a log-curvature calibration forces the cost to be exactly J. The addition law is the bridge that lets the uniqueness proof pass from the five plain conditions to the explicit formula.

DirectCoshAdd belongs on the cost uniqueness page because it is the form of the composition law that makes the proof work. It converts a functional equation about ratios into a functional equation about shifts, and that converted form is what connects to the hyperbolic cosine and its uniqueness. The page's main theorem, law_of_logic_forces_jcost, relies on this passage through log coordinates to reach the conclusion that only one cost function survives the five conditions.

THEOREM composition_law_equiv_coshAdd · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM Jcost_cosh_add_identity · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

The double-angle lemma

The cost uniqueness story does not depend on dAlembert_double as a separate premise. In the machine-checked development, dAlembert_double is a lemma derived from the composition law (the rule that costs combine by a fixed formula, not by taste) together with the normalization H 0 = 1. It states that for any function H satisfying the composition law, H (2 * t) = 2 * (H t)^2 - 1. The derivation is a direct algebraic consequence: it follows by substituting u = t into the composition identity H (t+u) + H (t-u) = 2 * H t * H u.

Because dAlembert_double is derived, not assumed, the main theorem law_of_logic_forces_jcost does not list it among its hypotheses. That theorem shows that any function F satisfying reciprocal symmetry, normalization, the composition law, calibration, and continuity must equal the cost function J(x) = (x + 1/x)/2 - 1. The proof route passes through the composition law, which is equivalent to a hyperbolic-cosine addition identity, and then through a d'Alembert equation whose solution is forced to be cosh. The double-angle lemma is one of several algebraic tools used inside that route, but it is not a load-bearing axiom.

If dAlembert_double were false, that would mean the composition law itself was inconsistent, since the lemma is a theorem of it. If the lemma were merely dropped from the library, the uniqueness proof would still go through, because the proof does not rely on it as an unproved assumption. The same holds for the other helper lemmas such as dAlembert_product and dAlembert_diff_square: they are consequences of the same composition law, not independent requirements. The five plain conditions are what force the cost function; the lemmas are the working parts of that forcing, not extra conditions on it.

THEOREM dAlembert_double · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM composition_law_equiv_coshAdd · IndisputableMonolith/Cost/FunctionalEquation.lean

Continuity at the origin

Recognition costs, the amounts posted when something is recognized, are forced into one formula by five plain conditions. The proof of that forcing result reaches a differential equation in log coordinates, where the transformed function H(t) = F(e^t) + 1 must satisfy H'' = H. To conclude that H is cosh, the proof needs to rule out other solutions. The lemma tendsto_H_one_of_log_curvature is a small but necessary step in that exclusion.

In plain language, the lemma says this: if a function H has value 1 at 0, and if its log-curvature (the limit of 2(H(t) - 1)/t² as t approaches 0) exists, then H(t) tends to 1 as t tends to 0. The function is continuous at the origin. This is not an axiom. It is a derived theorem, established from the definition of HasLogCurvature together with the initial condition H(0) = 1. The proof uses the fact that the curvature limit is taken at 0, so the numerator 2(H(t) - 1) must vanish as t goes to 0.

The lemma belongs on the cost uniqueness page because it supplies the continuity at zero that the uniqueness argument needs. The differential equation H'' = H has many solutions, but the ones that matter are those compatible with the recognition conditions. The condition H(0) = 1 is given. The log-curvature condition is also given. The lemma converts those two into a continuity fact, which is one of the ingredients the proof uses to select cosh as the only solution. It is a quiet lemma, but it closes a gap that would otherwise leave the uniqueness claim incomplete.

THEOREM tendsto_H_one_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM tendsto_H_one_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

The Compositional Bridge

Recognition (the posting of a cost when something is recognized) is governed by a cost function that must satisfy five plain conditions. The theorem law_of_logic_forces_jcost proves that any cost function meeting all five must equal J(x) = (x + 1/x)/2 - 1. One of those five conditions is the composition law, SatisfiesCompositionLaw, which states how costs combine when two events compose. The identity CoshAddIdentity is not a sixth condition; it is a restatement of that same composition law after a change of variables.

The change of variables is the log-coordinate reparametrization: G_F(t) = F(exp t). In these coordinates, the composition law becomes the identity CoshAddIdentity, which says that G_F(t+u) + G_F(t-u) equals 2 * (G_F t * G_F u) + 2 * (G_F t + G_F u). The theorem composition_law_equiv_coshAdd proves that a function satisfies the composition law if and only if it satisfies CoshAddIdentity. So the two are logically equivalent; dropping one is dropping the other.

What breaks is the proof chain. The uniqueness proof does not use the composition law directly in its multiplicative form. It uses CoshAddIdentity to enter the additive world, where the equation becomes a d'Alembert functional equation. From there, the proof derives that G_F must be cosh(t) - 1, which forces J(x). The theorem composition_logCurvature_forces_jcost shows that composition plus a fixed log-curvature of 1 already forces J(x), and the full theorem law_of_logic_forces_jcost assembles all five conditions. Without CoshAddIdentity, the bridge to the d'Alembert equation is gone, and the remaining conditions do not select a unique cost function.

The consequence is structural. The five conditions are not five independent constraints that happen to intersect at J(x). The composition law is the one that carries the additive structure; the other conditions (reciprocal symmetry, normalization, calibration, continuity) set the scale and regularity but do not by themselves force the cosh shape. Removing CoshAddIdentity leaves a much larger family of possible cost functions, and the uniqueness theorem no longer holds.

THEOREM composition_law_equiv_coshAdd · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

The ODE uniqueness lemma

The lemma ode_cosh_uniqueness is a statement about ordinary differential equations. It says that if a twice-differentiable function H satisfies the equation H''(t) = H(t) for every t, starts at H(0) = 1, and has first derivative zero at zero, then H is exactly the hyperbolic cosine, cosh. No other smooth function can satisfy those three conditions together. The proof in the machine-checked library first extracts continuity and differentiability from the equation itself, then promotes that regularity to twice-differentiability, and finally applies a standard uniqueness result for second-order linear ODEs.

This lemma belongs on the cost uniqueness page because it is the last step of the forcing chain. The uniqueness theorem for the cost function J(x) = (x + 1/x)/2 - 1 is established from five conditions: reciprocal symmetry, normalization, the composition law, calibration, and continuity. The proof transforms the cost into log coordinates, where the composition law becomes a d'Alembert functional equation. That equation, together with a regularity package drawn from Aczél theory, leads to the differential equation H'' = H. The initial conditions H(0) = 1 and H'(0) = 0 come from normalization and from the evenness forced by reciprocal symmetry. Applying ode_cosh_uniqueness then yields H = cosh, and translating back gives the cost function J. The lemma is therefore not a separate result; it is the bridge that turns the functional equation into the explicit formula.

What the lemma adds is precision about the role of regularity. Continuity alone does not force the differential equation; the proof needs a second derivative. The Aczél smoothness package supplies that extra regularity as hypotheses. The lemma itself is cleanly stated: given twice-differentiability and the ODE, uniqueness follows. It is a theorem in the machine-checked library, established without RS-specific axioms, and it anchors the final equality in the main uniqueness proof.

THEOREM ode_cosh_uniqueness · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM Jcost_G_eq_cosh_sub_one · IndisputableMonolith/Cost/FunctionalEquation.lean

The regularity bridge

The uniqueness theorem forces the cost function to be J(x) = (x + 1/x)/2 - 1 from five conditions, one of which is mere continuity. The proof cannot pass directly from continuity to the second-order differential equation whose solution is cosh. The gap is bridged by a package of regularity hypotheses drawn from Aczél theory, and cosh_dAlembert_to_ODE is the piece that confirms the bridge holds for the model solution itself.

In log coordinates, the cost function becomes H(t) = F(e^t) + 1, and the composition law becomes the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u). The theorem dAlembert_cosh_solution_of_log_curvature shows that if H satisfies this equation, has log curvature 1, and meets five regularity hypotheses, then H is Real.cosh. The regularity hypotheses are not free; each must be verified for the candidate solution. The declaration cosh_dAlembert_to_ODE is exactly that verification for one of the five: it proves that Real.cosh satisfies dAlembert_to_ODE_hypothesis, meaning that from the d'Alembert equation plus the initial condition deriv (deriv H) 0 = 1, the full ODE deriv (deriv H) t = H t follows.

The contribution is therefore not a new theorem about the cost function. It is a completeness check on the proof infrastructure. Without cosh_dAlembert_to_ODE, the chain from the d'Alembert equation to the ODE would have an unverified step for the very function that the uniqueness theorem claims to select. With it, the regularity package is closed: the model solution satisfies every hypothesis the derivation demands. The page should use it, not as a headline result, but as the supporting lemma that makes the uniqueness proof self-contained.

THEOREM cosh_dAlembert_to_ODE · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_cosh_solution_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

The role of cosh_initials

The declaration cosh_initials is a theorem in the machine-checked development that states two plain facts about the hyperbolic cosine: at zero it has value one, and its first derivative at zero is zero. These are exactly the initial conditions that the uniqueness proof needs when it solves the differential equation whose solution is forced to be cosh. The theorem is not a new assumption. It is a derived check that the candidate solution satisfies the conditions the proof requires.

On the cost uniqueness page, the main theorem law_of_logic_forces_jcost derives the cost function from five axioms. The proof passes through a change of variables into log coordinates, where the cost becomes a function H with H(0) = 1 and derivative zero at zero. The theorem ode_cosh_uniqueness then uses those two initial conditions together with the differential equation to conclude H is cosh. The declaration cosh_initials supplies exactly those two facts for the candidate. It is a small verification that the solution the proof reaches is consistent with the initial conditions it assumed.

The page should include cosh_initials as a supporting lemma, not as a premise. Its role is to close a gap in the proof narrative: it shows that the function that solves the differential equation also satisfies the initial conditions, so the uniqueness theorem applies. Without it, a reader might wonder whether the initial conditions are compatible with the equation. The theorem is derived directly from the standard facts Real.cosh_zero and Real.deriv_cosh, so it carries no extra assumptions. It is a check, not a contribution to the forcing chain.

THEOREM cosh_initials · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM cosh_initials · IndisputableMonolith/Cost/FunctionalEquation.lean

The evenness lemma

Recognition costs obey a symmetry: recognizing a ratio costs the same as recognizing its reciprocal. The theorem G_even_of_reciprocal_symmetry converts that symmetry into a fact about a transformed function. In log coordinates, where a ratio x becomes the shift t = log x, the cost function G(t) satisfies G(t) = G(-t). The function is even.

This evenness is not a separate assumption. It is derived from the reciprocal symmetry axiom alone. The proof is direct: substituting the reciprocal relation into the definition of G and using the logarithm identity log(1/x) = -log x yields the equality. The theorem statement in the machine-checked library records this as reciprocal_implies_G_even, which calls the lemma G_even_of_reciprocal_symmetry.

Why does this belong on the cost uniqueness page? The uniqueness proof for the cost function J(x) = (x + 1/x)/2 - 1 requires an initial condition in log coordinates: the derivative of H(t) = F(e^t) + 1 must be zero at t = 0. That condition is not one of the five stated axioms. It follows from evenness. An even differentiable function has derivative zero at the origin, so the reciprocal symmetry axiom supplies the missing initial condition through this lemma. The evenness lemma is the bridge from the symmetry axiom to the differential equation whose solution is cosh.

The lemma is therefore a load-bearing step in the chain that forces the unique cost function. It shows that one of the five plain conditions, reciprocal symmetry, does double duty: it shapes the function globally and fixes the local behavior at the origin needed for the uniqueness argument.

THEOREM reciprocal_implies_G_even · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM reciprocal_implies_G_even · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

The role of deriv_neg_self_zero

The cost uniqueness page currently does not cite deriv_neg_self_zero, and that is the correct choice. The declaration is a helper lemma in the machine-checked proof of ode_cosh_uniqueness_contdiff. It states that if a twice continuously differentiable function f satisfies deriv (deriv f) t = f t for all t, with f 0 = 0 and deriv f 0 = 0, then f is identically zero.

That lemma is one way to exclude the zero solution when solving the differential equation H'' = H. The uniqueness proof needs to show that the only solution with H 0 = 1 and deriv H 0 = 0 is cosh. The standard route applies ode_zero_uniqueness to the difference of two candidate solutions, which reduces the problem to the zero case. The declaration deriv_neg_self_zero is a variant of that same exclusion, packaged for a different formulation of the hypothesis.

For the encyclopedia page, the relevant fact is the final theorem ode_cosh_uniqueness_contdiff, which already carries the full weight of the uniqueness step. The internal helper deriv_neg_self_zero does not add a new mathematical fact about the cost function. It is an implementation detail of the proof script. Including it on the page would clutter the exposition without changing what the reader learns about the forcing result.

The page should stay focused on the theorems that state the uniqueness of the cost function and the lemmas that are directly cited in that statement. The helper lemmas that only appear inside proof scripts are better left out of the permanent reference.

THEOREM ode_cosh_uniqueness_contdiff · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness_contdiff · IndisputableMonolith/Cost/FunctionalEquation.lean

The missing unit

Imagine a ruler whose markings tell you the shape of every measurement but never say how long one unit is. The Lean uniqueness theorem proves that the cost function has the form J(x) = (x + 1/x)/2 - 1 once reciprocal symmetry, normalization, the composition law, calibration, and continuity are supplied. The paper's new question is whether calibration itself can be replaced by a structural rule.

Its answer is conditional and sharply divided by the space of ratios. On the countable carrier, meaning the discrete family of ratios supported by the framework, the paper derives on paper that the cheapest cost which charges any distinction is the exponent-one member, the canonical cost above. This turns the unit from a stipulated value into a leastness principle: compare admissible costs pointwise on positive ratios, and choose the one that is no larger than every other nondegenerate candidate. The paper also derives on paper that this leastness condition is equivalent to anchoring the cost at any one non-unit ratio, so the old anchor is identified as a consequence of the ordering rather than an independent physical choice.

The paper adds the boundaries that the Lean uniqueness chain does not state. It derives on paper that every nonnegative integer exponent gives an admissible cost, including even exponents, and that the zero-exponent sign cost charges nothing. Therefore the leastness rule must explicitly exclude the degenerate branch, or it selects a cost that prices no distinction. It also derives on paper that the completed real line has no cheapest positive exponent: costs can always be lowered by halving the exponent, while their infimum is the zero cost. The countable carrier has a bottom because its exponents are discrete; the continuum does not.

Finally, the paper reports a classification program for the countable candidates and states openly that its use of the six exponentials theorem is a named hypothesis, not a result proved in the paper. Its contribution is therefore a scale-selection principle, a discrete-versus-continuous boundary, and explicit nondegeneracy and transcendence conditions. It does not replace the Lean theorem's proof of the cost's shape, and it does not turn those paper arguments into Lean theorems.

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

The Role of the Limit Lemma

The lemma tendsto_H_one_of_log_curvature states that if a function H satisfies H(0) = 1 and has log-curvature κ at 0, then H tends to 1 as its argument tends to 0. It is not an axiom. It is a derived theorem, established from the definition of HasLogCurvature together with the initial condition H(0) = 1. The proof uses the fact that the curvature limit is taken at 0, so the numerator 2 * (H t - 1) must tend to 0 for the quotient to have a finite limit.

If the lemma were false, the entire uniqueness story would collapse at its first step. The theorem dAlembert_continuous_of_log_curvature, which derives continuity of H from the composition law and the curvature condition, relies on this limit to establish continuity at 0. Without continuity, the Aczél regularity hypotheses cannot be applied, and the chain from the composition law to the differential equation whose solution is cosh would be broken. The final theorem law_of_logic_forces_jcost, which forces the cost function to be J(x) = (x + 1/x)/2 - 1, depends on this chain.

In the actual development the lemma holds, so the story is intact. The curvature condition, together with the composition law, is strong enough to force continuity, and from there the uniqueness proof proceeds. The lemma is a load-bearing but derived piece of the argument, not an independent premise. Its role is to show that the log-curvature hypothesis, which is a local condition at 0, already implies the global continuity that the regularity package needs.

THEOREM tendsto_H_one_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_continuous_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

The zero-solution lemma

The uniqueness proof for the cost function J(x) = (x + 1/x)/2 - 1 reaches a differential equation in log coordinates: the transformed function H(t) = F(e^t) + 1 must satisfy H'' = H. To conclude that H is cosh, the proof needs to rule out other solutions. The declaration ode_zero_uniqueness is the lemma that performs this exclusion. It states that if a twice continuously differentiable function f satisfies f'' = f, with f(0) = 0 and f'(0) = 0, then f is identically zero.

This lemma is not one of the five axioms that force the cost function. It is a theorem about the differential equation itself, machine-checked inside the development. Its role is to make the final step of the uniqueness argument precise: once the difference between two candidate solutions is shown to satisfy the zero initial conditions, the lemma forces that difference to vanish, leaving a single solution. Without it, the proof would have to argue uniqueness of the differential equation by other means, or leave a gap in the chain from the composition law to cosh.

The lemma contributes to the internal structure of the proof, not to the statement of the uniqueness theorem. The page's central claim, that any cost function meeting the five conditions must equal J, is already established by law_of_logic_forces_jcost. The zero-solution lemma is one of the tools that makes that theorem go through, alongside the regularity hypotheses drawn from Aczél theory. It belongs on the page as a supporting fact, not as a separate premise.

THEOREM ode_zero_uniqueness · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_zero_uniqueness · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

The Cosh Addition Identity

The theorem Jcost_cosh_add_identity states that the cost function J(x) = (x + 1/x)/2 - 1 obeys a particular algebraic relation when its argument is expressed in log coordinates. In those coordinates, where a ratio x becomes the shift t = log x, the transformed cost G(t) = J(e^t) satisfies the identity G(t+u) + G(t-u) = 2 * G(t) * G(u) + 2 * (G(t) + G(u)) for all real t and u. This is the CoshAddIdentity, so named because the same relation holds for the hyperbolic cosine after a shift by one: cosh(t+u) + cosh(t-u) = 2 * cosh(t) * cosh(u), and the extra linear terms in the cost version arise from the -1 in J.

The identity belongs on the cost uniqueness page because it is the bridge between the composition law and the differential equation. The composition law for a recognition cost F states that F(x*y) + F(x/y) = 2 * F(x) * F(y) + 2 * F(x) + 2 * F(y) for positive x and y. In log coordinates this law is exactly the CoshAddIdentity. The theorem composition_law_equiv_coshAdd proves the equivalence: a function satisfies the composition law if and only if its log-coordinate transform satisfies the CoshAddIdentity. The identity is therefore not an extra assumption; it is the composition law in a different coordinate system.

Once the identity is in place, the uniqueness proof proceeds by showing that the transformed function H(t) = F(e^t) + 1 satisfies the d'Alembert equation H(t+u) + H(t-u) = 2 * H(t) * H(u), and from there a differential equation H'' = H with initial conditions H(0) = 1 and H'(0) = 0. The lemma ode_cosh_uniqueness_contdiff then forces H to be cosh, which gives J as the unique cost. The Jcost_cosh_add_identity theorem confirms that the candidate J itself satisfies the identity, closing the loop: the composition law forces the identity, and the identity forces the unique solution.

THEOREM Jcost_cosh_add_identity · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM Jcost_cosh_add_identity · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM composition_law_equiv_coshAdd · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness_contdiff · IndisputableMonolith/Cost/FunctionalEquation.lean

The uniqueness lemma

The machine-checked lemma ode_cosh_uniqueness_contdiff states a fact about ordinary differential equations. If a function H is twice continuously differentiable, if its second derivative equals the function itself at every point, if H(0) = 1, and if the first derivative at zero is 0, then H is the hyperbolic cosine function cosh. The proof is a theorem in Lean 4, verified with no gaps and no extra axioms.

This lemma belongs on the cost uniqueness page because it closes the last gap in the forcing argument. The derivation of the unique cost function J(x) = (x + 1/x)/2 - 1 reaches a differential equation in log coordinates: the transformed function H(t) must satisfy H'' = H. The equation alone does not pin down H; other functions also satisfy it. The two initial conditions H(0) = 1 and H'(0) = 0, together with the smoothness assumption, are what force the solution to be cosh. Without this lemma, the uniqueness proof would be incomplete.

The lemma is used at the end of the chain that proves the main forcing theorem. It is a standard result from the theory of linear differential equations, but here it is formalized and checked in the same framework as the rest of the cost derivation. The declaration ode_cosh_uniqueness_contdiff is the precise statement that makes the conclusion rigorous: given the equation and the initial conditions, no other twice continuously differentiable function can satisfy them.

THEOREM ode_cosh_uniqueness_contdiff · IndisputableMonolith/Cost/FunctionalEquation.lean

The zero derivative at zero

The lemma even_deriv_at_zero states a plain fact about a function that is even and twice continuously differentiable: if its value at zero is zero and its derivative at zero is zero, then the function is identically zero. In the cost uniqueness proof, this lemma is applied to a difference of two candidate solutions. The difference inherits the differential equation from the candidates, and its initial conditions at zero are both zero, so the lemma forces the difference to vanish everywhere.

This lemma belongs on the cost uniqueness page because it is the step that rules out non-cosh solutions. The uniqueness proof reaches a differential equation in log coordinates, where the transformed function H(t) = F(e^t) + 1 must satisfy H'' = H. To conclude that H is cosh, the proof needs to exclude other solutions of the same equation. The lemma ode_zero_uniqueness performs that exclusion: it states that if a twice continuously differentiable function f satisfies deriv (deriv f) t = f t for all t, with f 0 = 0 and deriv f 0 = 0, then f is identically zero. This is the same structure as even_deriv_at_zero, applied in the proof of ode_cosh_uniqueness_contdiff.

The consequence is that the differential equation H'' = H, together with the initial conditions H(0) = 1 and H'(0) = 0, has exactly one solution: the hyperbolic cosine. The lemma even_deriv_at_zero is not itself a theorem about the cost function; it is a helper lemma in the machine-checked proof of ode_cosh_uniqueness_contdiff. Its role is to close off the alternative solutions, leaving cosh as the only candidate that survives the forcing chain.

THEOREM ode_zero_uniqueness · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_zero_uniqueness · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness_contdiff · IndisputableMonolith/Cost/FunctionalEquation.lean

The regularity step

The lemma cosh_satisfies_continuous states, in plain terms, that the hyperbolic cosine function is continuous on the real line. That fact is a standard property of the function, but in the Recognition Science proof it is not a background assumption. It is a machine-checked theorem that supplies one of the regularity hypotheses required by the uniqueness theorem for the cost function.

The cost uniqueness proof reaches a differential equation in log coordinates. The transformed function H(t) = F(e^t) + 1 must satisfy H'' = H, and the proof must rule out other solutions. The lemma ode_cosh_uniqueness_contdiff performs that exclusion: if a twice continuously differentiable function H satisfies the equation, with H(0) = 1 and H'(0) = 0, then H is cosh. The continuity of cosh is one of the ingredients that the broader uniqueness theorem needs in order to apply. The declaration cosh_satisfies_continuous is the specific proof that the candidate function meets that continuity condition.

The lemma belongs on the cost uniqueness page because it closes a gap in the forcing argument. The page's central result, that the cost function must equal J(x) = (x + 1/x)/2 - 1, depends on showing that the only solution worth selecting is cosh. That selection step requires several regularity checks on the candidate. The continuity lemma is one of those checks, and it is established directly from the definition of cosh rather than assumed. Without it, the uniqueness theorem would have an unfulfilled hypothesis, and the forcing chain would not close.

THEOREM cosh_satisfies_continuous · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness_contdiff · IndisputableMonolith/Cost/FunctionalEquation.lean

Continuity from log curvature

The declaration dAlembert_continuous_of_log_curvature is a theorem in the machine-checked proof of cost uniqueness. It states that a function H satisfying the cosine addition identity, with H(0) = 1 and having log-curvature at 0, is continuous everywhere. The log-curvature condition is the calibration input: it fixes the local scale of recognition near the identity. Continuity is the regularity that lets later steps move from the addition identity to the differential equation H'' = H.

The cost uniqueness page should not cite this lemma, because the page's main theorem already carries continuity as an explicit hypothesis. The forcing result law_of_logic_forces_jcost takes ContinuousOn F (Set.Ioi 0) as one of its five plain conditions. In the log-coordinate proof, that continuity is passed forward into the regularity hypotheses that the cosh solution requires. The lemma dAlembert_continuous_of_log_curvature would be needed only in a variant proof that replaced the continuity hypothesis with log-curvature and then derived continuity from it. The page does not use that variant, so citing the lemma would add a redundant path without changing the statement.

The lemma remains useful as a structural fact about the framework. It shows that calibration plus the addition identity already imply the continuity that other arguments assume. That is a genuine derivation, not a definitional choice. But it is a supporting result for alternative proof routes, not a step in the proof the page presents. Leaving it off the page is the correct choice, and the declaration should stay in the module as a helper for any future variant that weakens the continuity hypothesis.

THEOREM dAlembert_continuous_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

Regularity bridge

The cost uniqueness proof reaches a differential equation in log coordinates: the transformed function H(t) = F(e^t) + 1 must satisfy H'' = H. To conclude that H is cosh, the proof must rule out other solutions. The declaration ode_regularity_differentiable_of_smooth is one of the regularity hypotheses used in that exclusion step. It states, in effect, that a smooth function satisfying the equation is differentiable, which is a bridge from a smoothness assumption to a differentiability conclusion.

In the library, the uniqueness theorem ode_cosh_uniqueness takes five regularity hypotheses as inputs. One of them, ode_regularity_differentiable_hypothesis, is exactly the kind of assumption that ode_regularity_differentiable_of_smooth would supply. The theorem dAlembert_cosh_solution_of_log_curvature and its variant dAlembert_cosh_solution both list this differentiability hypothesis among their premises. The declaration itself is not a theorem about the cost function; it is a generic regularity bridge, likely used inside the proof of a lemma that turns a smoothness condition into the differentiability condition the uniqueness argument requires.

For the cost uniqueness page, this declaration should stay off the page as a standalone claim. The page's subject is the forcing result: five plain conditions force the cost formula J(x) = (x + 1/x)/2 - 1. A regularity bridge is a technical step inside that proof, not a fact a reader needs to verify independently. The page already cites the theorems that use it, such as ode_cosh_uniqueness and dAlembert_cosh_solution. Adding ode_regularity_differentiable_of_smooth as a separate claim would duplicate the proof chain without adding a new fact about the cost function.

What the declaration contributes is internal: it is part of the machine-checked scaffolding that makes the uniqueness proof go through. The page should mention that the proof uses regularity hypotheses, but it should not list this helper as a claim. The honest placement is in the proof apparatus, not in the prose.

THEOREM ode_cosh_uniqueness · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_cosh_solution_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

The Taylor lemma

The declaration taylorWithinEval_one_univ is a general Taylor expansion lemma from the library. It is not used in the machine-checked proof of the cost uniqueness theorem cost uniqueness, the result that any cost function satisfying the five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The proof reaches a differential equation in log coordinates, where the transformed function H(t) = F(e^t) + 1 must satisfy H'' = H, and it rules out other solutions with the dedicated lemma ode_cosh_uniqueness_contdiff, not with a Taylor expansion.

Leaving taylorWithinEval_one_univ off the page is the correct choice. The page's purpose is to present the forcing chain that derives the unique cost formula, and every lemma cited there has a specific role in that chain. A general Taylor lemma would add no information about why the cost function is unique. It would only distract from the actual structure of the proof, which turns on the d'Alembert equation and the uniqueness of the solution to H'' = H with the initial conditions H(0) = 1 and H'(0) = 0.

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness_contdiff · IndisputableMonolith/Cost/FunctionalEquation.lean

The hidden addition rule

Imagine you are keeping books for the universe. Every time something is recognized, the ledger posts a cost, a number that says how expensive that recognition was. The uniqueness proof on this page shows that only one cost function survives five plain conditions. But the proof has a secret passage: a change of variables that turns the cost into a shape where addition becomes visible.

That passage is what CoshAddIdentity names. Write the cost as a function of a ratio, then switch to logarithms, so multiplication of ratios becomes addition of logarithms. In those coordinates the cost becomes a curve, and CoshAddIdentity says that curve obeys the same addition rule as the hyperbolic cosine: the value at a sum plus the value at a difference equals twice the product of the two values, plus two copies of each. It is the identity that makes the curve recognizable as cosh minus one, and therefore makes the cost itself recognizable as J(x) = (x + 1/x)/2 - 1.

Why does this belong on the cost uniqueness page? Because it is the hinge. The Lean proof of uniqueness, law_of_logic_forces_jcost, takes the five conditions and forces the cost to equal J. One of those conditions, the composition law, is exactly equivalent to CoshAddIdentity: a theorem in the library proves the two statements are interchangeable. So the addition rule is not a separate assumption smuggled in; it is the composition law wearing a different coat. Once the cost satisfies that rule, the rest of the proof is a known path: the curve must be cosh, and the cost must be J.

The practical effect is that the whole uniqueness argument can be read as a single sentence: the five conditions force the cost to satisfy the cosh addition rule, and the cosh addition rule forces the cost to be J. That is what makes the page's central claim feel less like a list of lemmas and more like one continuous push. The reader who sees the addition rule has seen the engine of the proof.

THEOREM composition_law_equiv_coshAdd · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM Jcost_cosh_add_identity · IndisputableMonolith/Cost/FunctionalEquation.lean

The role of cosh_initials

Recognition costs, the amounts posted when something is recognized, are forced into one formula by five plain conditions. The proof of that forcing result reaches a differential equation in log coordinates, where the transformed function H(t) = F(e^t) + 1 must satisfy H'' = H. The equation alone does not select a unique function. It admits many solutions, including exponential combinations and zero. To conclude that H is the hyperbolic cosine, the proof needs two boundary conditions: H(0) = 1 and H'(0) = 0. The theorem cosh_initials supplies exactly those two facts for the candidate solution.

The boundary conditions are not optional decoration. The machine-checked lemma ode_cosh_uniqueness_contdiff states the full uniqueness result: if a twice continuously differentiable function H satisfies H'' = H at every point, with H(0) = 1 and H'(0) = 0, then H is cosh. Remove either initial condition and the conclusion fails. With H(0) = 1 but no condition on the first derivative, the shifted hyperbolic sine functions sinh(t) + cosh(t) also solve the equation. With H'(0) = 0 but no condition at zero, scaled cosines and hyperbolic cosines of different amplitudes remain possible. The two initial conditions together collapse the family to one member.

If cosh_initials were false, the proof of the uniqueness theorem could not go through. The lemma is not an axiom; it is a derived theorem, established from the standard definitions of cosh and sinh. Its content is the elementary fact that cosh(0) = 1 and the derivative of cosh at zero is 0. If the lemma were dropped from the library, the uniqueness theorem would lose its boundary conditions and the forcing chain would stop before reaching J(x) = (x + 1/x)/2 - 1. The cost uniqueness story would be incomplete at the point where the differential equation is solved.

THEOREM cosh_initials · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness_contdiff · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM cosh_initials · IndisputableMonolith/Cost/FunctionalEquation.lean

The d'Alembert route

The declaration dAlembert_cosh_solution_of_log_curvature is a theorem that derives the same cosh conclusion as the ODE route, but from the d'Alembert functional equation instead of a second-order differential equation. It states that if a function H satisfies H(0) = 1, obeys the d'Alembert equation H(t+u) + H(t-u) = 2 * H t * H u for all t and u, has log-curvature κ at 0, and has second derivative 1 at 0, then H is the hyperbolic cosine function cosh. The theorem is established in Lean, with the regularity hypotheses packaged as named assumptions.

The cost uniqueness page should not cite this declaration as a standalone result. The page's main theorem, law_of_logic_forces_jcost, already forces the cost function J(x) = (x + 1/x)/2 - 1 from the five plain conditions. That proof reaches the differential equation H'' = H in log coordinates, and then uses ode_cosh_uniqueness_contdiff to conclude H is cosh. The d'Alembert route is an alternative path to the same conclusion: it starts from the composition law, which is equivalent to the d'Alembert equation in log coordinates, and derives the same cosh result through a different chain of lemmas. Both routes are established, but the page already presents the ODE route as the direct proof of the main theorem.

The d'Alembert route does contribute to the framework's robustness. It shows that the cosh conclusion does not depend on the specific path taken after the composition law: whether one goes through the second-order ODE or through the d'Alembert equation, the result is the same. This is a structural fact about the proof, not a new theorem about the cost function itself. The page's main theorem already states the full forcing result; the d'Alembert route is a supporting lemma that confirms the uniqueness from a different angle. It should stay in the library as a verified alternative, but it does not need to be cited on the cost uniqueness page unless the page discusses the proof structure in detail.

THEOREM dAlembert_cosh_solution_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_cosh_solution_of_log_curvature · IndisputableMonolith/Cost/FunctionalEquation.lean

Why only one cost

Imagine you are keeping books for the universe. Every time something is recognized, the ledger posts a cost. The cost of doing nothing must be zero. The cost of swapping a ratio for its reciprocal must be the same cost (looking both ways is free). And when two events compose, their costs combine by a fixed rule, not by taste. Ask which functions of a positive number obey those rules and one more, a unit of curvature that sets the scale. The answer is not a family. It is a single function: J(x) = (x + 1/x)/2 - 1.

That uniqueness is the load-bearing fact beneath most of Recognition Science. If many costs were allowed, every later prediction would hide a free parameter. Because only J survives, the price of a prime, the shape of a particle mass ladder, and the reading of the Riemann Hypothesis as a conservation law all inherit the same spine. The proof lives in the library as a chain of ordinary functional equations, not as a new axiom.

The argument, said without symbols first: reciprocity makes the cost even in logarithmic coordinates, so it cannot prefer one direction over its opposite. Normalization pins the cost of a perfect match at zero. Continuity upgrades the solution from merely continuous to smooth. The curvature condition then fixes the second derivative at the origin, which is enough to force the unique solution of the resulting differential equation to be the hyperbolic cosine. Translating back from log coordinates gives J.

In symbols, the composition law becomes the d'Alembert equation after a short change of variables. Reciprocal symmetry makes G even; setting F(1) = 0 gives G(0) = 0; writing H = G + 1 gives H(0) = 1. Under the regularity package used for the classification, any continuous solution of that equation with H(0) = 1 is smooth. Evenness forces H'(0) = 0, and unit log curvature fixes H''(0) = 1. The equation H'' = H with those initial data has the unique solution H(t) = cosh t, so G(t) = cosh t - 1, which is J in the original variable. THEOREM

What this page is really saying is small and large at once. Small: a classical functional equation, proved carefully, forces one formula. Large: the theory does not get to choose how expensive recognition is. The cost is part of the furniture of the ledger, the way primes are part of the furniture of multiplication.

THEOREM composition_logCurvature_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM composition_law_equiv_coshAdd · H · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM reciprocal_implies_G_even · normalized_implies_G_zero · H · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM dAlembert_smooth_of_aczel · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM even_deriv_at_zero · deriv2_of_logCurvature · IndisputableMonolith/Cost/FunctionalEquation.lean

THEOREM ode_cosh_uniqueness_contdiff · Jcost_G_eq_cosh_sub_one · IndisputableMonolith/Cost/FunctionalEquation.lean

The paper's added case

Imagine testing a rule for keeping books about change. The Lean chain already proves that five stated conditions select one cost, J(x) = (x + 1/x)/2 - 1. The paper adds a different kind of value: it turns that result into a self-contained mathematical argument that a reader can follow without opening the formal library.

Its main strengthening is about regularity. The Lean theorem is stated with continuity on the positive reals and an Aczel smoothness package. On paper, the manuscript derives continuity, then C2 regularity, from the composition identity and the quadratic calibration itself. The proof moves to log-coordinates, where multiplication becomes addition and the law becomes the d'Alembert equation. A central-difference argument then yields the differential equation needed to identify the solution. In this presentation, smoothness is a consequence of the functional law and its calibration, rather than a condition supplied from outside.

The manuscript also records the full calibrated classification on paper. For positive curvature the lifted function is a hyperbolic cosine with the corresponding scale, for negative curvature it is an ordinary cosine with the corresponding scale, and for zero curvature it is constant. Unit calibration selects the hyperbolic-cosine case and therefore the canonical cost. That broader classification explains exactly what the calibration rules out, including the one-parameter rescaling that would otherwise remain.

Finally, the paper checks that the proposed cost really satisfies the stated conditions, including reciprocity, normalization, composition, and unit curvature, and prints all proofs in one place. Those are paper-only contributions, tagged DERIVED-UNFORMALIZED here. They make the theorem auditable as ordinary mathematics and clarify its scope. They do not replace the kernel-checked Lean result, and the paper's optional machine-check artifact is supplementary rather than its foundation.

THEOREM law_of_logic_forces_jcost · IndisputableMonolith/Cost/FunctionalEquation.lean

What this page does not claim

This answer does not claim that dropping even_deriv_at_zero alone breaks the proof while reciprocal symmetry remains intact, since reciprocal symmetry implies it. This answer does not claim that the d'Alembert equation has no other continuous solutions; the general solution family is stated without proof. This answer does not claim that the uniqueness theorem fails without the AczelSmoothnessPackage, only that the stated proof uses it. cosh_satisfies_differentiable is not a statement about the cost function itself, only about the candidate solution. The declaration does not replace the continuity hypothesis in the main uniqueness theorem. The regularity package is not part of the five plain conditions stated on the page. DirectCoshAdd is not a new axiom; it is equivalent to the composition law. This answer does not derive the full uniqueness proof from the five conditions. The log-coordinate reparametrization is not claimed to be unique among all possible coordinate changes. Not claiming that dAlembert_double is an axiom or a hypothesis of the uniqueness theorem. Not claiming that dropping dAlembert_double would change the set of functions satisfying the five conditions. Not claiming that the composition law is the only route to the cost function; the theorem also requires reciprocal symmetry, normalization, calibration, and continuity. This lemma does not by itself prove that H is cosh. This lemma does not establish the existence of log-curvature; it only uses it as a hypothesis. Not claiming that dropping CoshAddIdentity alone makes the theorem false; it is equivalent to dropping the composition law. Not claiming that the remaining four conditions are insufficient in some other proof route not present in the pack. Not claiming that CoshAddIdentity is an independent axiom; it is a derived equivalence. This answer does not claim that continuity alone forces the differential equation. This answer does not claim that the Aczél smoothness package is derived from the five stated axioms. This answer does not claim that the uniqueness lemma is a standalone result independent of the cost framework. Not claiming that cosh_dAlembert_to_ODE is a new result about the cost function itself; it is a regularity check on the model solution. Not claiming that the five regularity hypotheses are derived from the five cost axioms; they are an additional package drawn from Aczél theory. Not claiming that the page's uniqueness proof is invalid without this lemma; the claim is that its presence makes the proof self-contained. cosh_initials is not a premise of the uniqueness theorem. cosh_initials does not by itself force the cost function to be J. The page does not claim that cosh_initials is the only route to the initial conditions. Not claiming that evenness alone proves the uniqueness theorem. Not claiming that the zero-derivative condition is an axiom of the framework. This answer does not claim that deriv_neg_self_zero is a theorem about the cost function J. This answer does not claim that deriv_neg_self_zero is the only way to rule out the zero solution. The paper does not add a Lean-verified proof of its scale-selection or carrier-classification results. The six exponentials theorem is used as a named hypothesis rather than proved in the paper. The paper does not show that the completed real line has a least positive cost. This answer does not claim that dropping the lemma would leave the uniqueness theorem false; it only describes the dependency structure. This answer does not claim that the lemma is an independent axiom of the framework. The lemma ode_zero_uniqueness is not one of the five axioms that force the cost function. This answer does not claim that the zero-solution lemma alone proves the uniqueness theorem without the other hypotheses. This answer does not claim that the CoshAddIdentity itself is the composition law, only that the two are equivalent in log coordinates. This answer does not claim that the identity alone forces J; it is one step in a chain that also requires the other four conditions. This answer does not claim that ode_cosh_uniqueness_contdiff is the main forcing theorem; it is a supporting lemma. This answer does not claim that the differential equation alone determines cosh without the initial conditions. This answer does not claim that the lemma applies to functions that are not twice continuously differentiable. This answer does not claim that even_deriv_at_zero is a theorem about the cost function itself. This answer does not claim that the uniqueness proof is complete without the regularity hypotheses from the Aczél smoothness package. This answer does not claim that the lemma even_deriv_at_zero appears in the evidence pack as a standalone declaration. This answer does not claim that cosh_satisfies_continuous alone proves the uniqueness theorem. This answer does not claim that the continuity of cosh is an assumption rather than a established theorem. This answer does not claim that the cost uniqueness proof is complete without the other regularity lemmas. This answer does not claim that dAlembert_continuous_of_log_curvature is used in the page's proof. This answer does not claim that log-curvature alone is sufficient for the full forcing theorem. This answer does not claim that ode_regularity_differentiable_of_smooth is a theorem about the cost function itself. This answer does not claim that the declaration appears as a named premise in ode_cosh_uniqueness. This answer does not claim that taylorWithinEval_one_univ is false or unusable in other contexts. This answer does not claim that the cost uniqueness proof avoids all use of Taylor expansions in its regularity hypotheses. CoshAddIdentity is not a new assumption; it is equivalent to the composition law. This answer does not prove that the five conditions are independent of each other. Not claimed that dropping cosh_initials would produce a different valid cost function. Not claimed that cosh_initials is the only source of boundary conditions in the forcing chain. This answer does not claim the d'Alembert route is the main proof of the cost uniqueness theorem. This answer does not claim the d'Alembert route is simpler or more general than the ODE route. This answer does not claim the cost uniqueness page should be modified to include the d'Alembert theorem. Uniqueness outside the positive real numbers. A proof of the Aczel classification without the stated regularity package. An empirical fit of J to measured laboratory values. The paper does not replace the kernel-checked Lean proof. The paper does not claim that the broader Recognition Science framework is needed for this mathematical theorem. The optional machine-check artifact is not the foundation of the paper's argument.

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/FunctionalEquation.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: