module module high

`IndisputableMonolith.Cost.FunctionalEquation`

The module supplies the log reparametrization that converts the multiplicative Recognition Composition Law into an additive d'Alembert equation on the reals. Researchers handling T5 uniqueness or Aczel classification cite it for the change of variables from F to G_F. The module consists of definitions for G and H together with their symmetry and addition identities.

claimThe reparametrization is $G_F(t) := F(e^t)$ for a cost function F obeying the Recognition Composition Law.

background

The Cost domain encodes the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This module reparametrizes via logarithms to reach the d'Alembert form H(t+u) + H(t-u) = 2H(t)H(u) with H(0)=1. It imports the AczelClass typeclass whose doc-comment states: "This module declares the typeclass interface for the d'Alembert smoothness package and the bootstrap theorem that uses it."

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Feeds AczelClassification which packages the d'Alembert forcing chain and AczelTheorem which proves every continuous solution is C^∞. Also supports ContDiffReduction and FunctionalEquationAczel for the T5 J-uniqueness step in the forcing chain.

scope and limits

Does not prove continuity implies smoothness.
Does not classify all solutions of the functional equation.
Does not connect to the phi fixed point or eight-tick octave.
Does not derive the mass formula or alpha band.

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