module module moderate

`IndisputableMonolith.Cost.FunctionalEquation`

Cost.FunctionalEquation supplies the log reparametrization converting the multiplicative cost functional equation into additive d'Alembert form. Modules handling Aczél classification and T5 uniqueness cite it to reduce the Recognition Composition Law to classical smoothness results. The module consists of the core definition G_F(t) := F(exp t) together with supporting evenness and derivative lemmas.

claim$G_F(t) := F(e^t)$ for a function $F$ obeying the Recognition Composition Law, together with the induced even function $H$ satisfying $H(t+u)+H(t-u)=2H(t)H(u)$ and $H(0)=1$.

background

The module works inside the Cost domain after the Recognition Composition Law has been stated. It imports the AczelClass typeclass interface that packages the d'Alembert smoothness bootstrap. The central object is the change-of-variable $G_F(t)=F(e^t)$ that turns the multiplicative arguments of the original equation into additive arguments, allowing direct appeal to the classical d'Alembert equation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The reparametrization is used by AczelClassification, AczelProof and ContDiffReduction to obtain the ODE $H''=H$ and thereby close the T5 uniqueness step. Downstream modules such as CostAlgebra and CostUniqueness import it to separate the Aczél-dependent closure from the axiom-free core.

scope and limits

Does not derive the Recognition Composition Law.
Does not contain the Aczél smoothness proof itself.
Does not address the phi-ladder or mass formulas.
Does not treat the eight-tick octave or spatial dimension forcing.

used by (21)

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

IndisputableMonolith.Algebra.CostAlgebra module_import
IndisputableMonolith.Cost.AczelClassification module_import
IndisputableMonolith.Cost.AczelProof module_import
IndisputableMonolith.Cost.AczelTheorem module_import
IndisputableMonolith.Cost.ContDiffReduction module_import
IndisputableMonolith.Cost.FunctionalEquationAczel module_import
IndisputableMonolith.CostUniqueness module_import
IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction module_import
IndisputableMonolith.Foundation.AxiomDischargePlan module_import
IndisputableMonolith.Foundation.CostAxioms module_import
IndisputableMonolith.Foundation.DAlembert.Counterexamples module_import
IndisputableMonolith.Foundation.DAlembert.FourthGate module_import
IndisputableMonolith.Foundation.DAlembert.FullUnconditional module_import
IndisputableMonolith.Foundation.DAlembert.Proof module_import
IndisputableMonolith.Foundation.DAlembert.RightAffineFromFactorization module_import
IndisputableMonolith.Foundation.DAlembert.Stability module_import
IndisputableMonolith.Foundation.DAlembert.Ultimate module_import
IndisputableMonolith.Foundation.DAlembert.Unconditional module_import
IndisputableMonolith.Foundation.LogicAsFunctionalEquation module_import
IndisputableMonolith.Measurement.RecognitionAngle.AngleFunctionalEquation module_import
IndisputableMonolith.NumberTheory.ZeroCompositionInterface module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.AczelClass module_import

declarations in this module (62)

def G L23
def H L26
def CoshAddIdentity L29
def DirectCoshAdd L34
lemma CoshAddIdentity_implies_DirectCoshAdd L38
lemma G_even_of_reciprocal_symmetry L42
lemma G_zero_of_unit L51
theorem Jcost_G_eq_cosh_sub_one L54
theorem Jcost_cosh_add_identity L60
theorem even_deriv_at_zero L76
lemma dAlembert_even L97
lemma dAlembert_double L106
lemma dAlembert_product L121
lemma dAlembert_diff_square L139
def HasLogCurvature L156
lemma sub_one_eq_mul_ratio L159
lemma tendsto_H_one_of_log_curvature L166
theorem dAlembert_continuous_of_log_curvature L192
lemma deriv_exp_neg L280
lemma ode_diagonalization L291
lemma deriv_neg_self_zero L315
lemma deriv_pos_self_zero L342
theorem ode_zero_uniqueness L371
theorem cosh_second_deriv_eq L400
theorem cosh_initials L407
theorem ode_cosh_uniqueness_contdiff L414
def ode_linear_regularity_bootstrap_hypothesis L460
def ode_regularity_continuous_hypothesis L467
def ode_regularity_differentiable_hypothesis L474
theorem cosh_satisfies_bootstrap L484
theorem cosh_satisfies_continuous L489
theorem cosh_satisfies_differentiable L494
theorem ode_cosh_uniqueness L498
def dAlembert_continuous_implies_smooth_hypothesis L525
def dAlembert_to_ODE_hypothesis L535
theorem cosh_dAlembert_smooth L540
theorem cosh_dAlembert_to_ODE L545
theorem dAlembert_cosh_solution L549
theorem dAlembert_cosh_solution_of_log_curvature L569
def IsReciprocalCost L593
def IsNormalized L597
def IsCalibrated L601
def IsCalibratedLimit L606
lemma taylorWithinEval_succ_real L609
lemma taylorWithinEval_one_univ L616
lemma taylorWithinEval_two_univ L627
lemma isCalibratedLimit_of_isCalibrated L656
lemma isCalibrated_of_isCalibratedLimit L676
def SatisfiesCompositionLaw L700
theorem reciprocal_implies_G_even L705
theorem normalized_implies_G_zero L710
theorem composition_law_equiv_coshAdd L719
theorem washburn_uniqueness L761
def symmetric_second_diff_limit_hypothesis L859
theorem dAlembert_smooth_of_aczel L874
theorem dAlembert_to_ODE_general_theorem L882
theorem dAlembert_to_ODE_theorem L960
theorem ode_regularity_continuous_of_smooth L1035
theorem ode_regularity_differentiable_of_smooth L1040
theorem ode_regularity_bootstrap_of_smooth L1045
theorem dAlembert_cosh_solution_aczel L1053
theorem washburn_uniqueness_aczel L1076