module module high

`IndisputableMonolith.Algebra.CostAlgebra`

The CostAlgebra module defines the J-cost function as the explicit solution to the Recognition Composition Law and supplies its basic algebraic properties including composition operators. Researchers building the T5 uniqueness step or the subsequent phi-ring structures cite this module. The module proceeds by importing functional equation helpers and verifying the law through direct substitution into the closed form.

claim$J(x) = ½(x + x^{-1}) - 1$ satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ for all $x, y > 0$.

background

This module introduces the J-cost function that satisfies the Recognition Composition Law in the Recognition Science algebra layer. The upstream FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof, while FunctionalEquationAczel isolates Aczél-based closure theorems for compatibility with legacy callers. Key objects defined here include the explicit J, its evaluation at 1 and reciprocals, non-negativity, defect form, and the costCompose operation with commutativity and associativity up to defect.

proof idea

The module states the closed-form definition of J and verifies the Recognition Composition Law by algebraic expansion. It then defines the costCompose family and proves its algebraic properties directly from the law. This is a definition module with supporting verification lemmas rather than a deep theorem module.

why it matters in Recognition Science

The module feeds the PhiRing and RecognitionCategory constructions that build the self-similar algebraic structures. It realizes the T5 J-uniqueness step by exhibiting the explicit solution to the Recognition Composition Law. This supplies the algebraic foundation required before the phi-ladder and eight-tick octave appear in the forcing chain.

scope and limits

Does not prove uniqueness of J from the Recognition Composition Law.
Does not derive numerical constants such as alpha or G.
Does not address the phi-ladder mass formula or Berry threshold.
Does not reach the eight-tick octave or D = 3.

used by (2)

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

IndisputableMonolith.Algebra.PhiRing module_import
IndisputableMonolith.Algebra.RecognitionCategory module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import
IndisputableMonolith.Cost.FunctionalEquationAczel module_import

declarations in this module (94)

def J L63
theorem J_at_one L66
theorem J_reciprocal L71
theorem J_nonneg L75
theorem J_defect_form L79
def SatisfiesRCL L92
theorem RCL_holds L98
def costCompose L115
theorem costCompose_comm L121
theorem costCompose_assoc_defect L126
theorem costCompose_flexible L132
theorem costCompose_zero_left L136
theorem costCompose_zero_right L140
theorem costCompose_nonneg L146
theorem costCompose_factored L156
theorem costCompose_no_identity L161
theorem costCompose_power_assoc L175
theorem costCompose_fourfold_power_counterexample L179
def H L188
theorem H_at_one L191
theorem H_dAlembert L199
abbrev ShiftedCarrier L222
def shiftedCompose L225
def shiftedUnit L232
theorem shiftedUnit_val L236
theorem shiftedCompose_val L238
theorem H_ge_one L262
def shiftedOfH L268
abbrev ShiftedHValue L274
def shiftedComposeH L277
theorem shiftedComposeH_val L283
def shiftedHValueOf L298
def defectDist L310
theorem defectDist_self L313
theorem defectDist_symm L319
theorem defectDist_nonneg L328
theorem J_le_J_of_inv_le_le L336
theorem defectDist_le_J_of_ratio_bounds L361
theorem quasiTriangleConstant_eq L369
theorem defectDist_quasi_triangle_local L376
theorem defectDist_no_global_quasi_triangle L426
theorem costCompose_sub_left L490
theorem costCompose_left_cancel L496
theorem costCompose_right_cancel L509
def PositiveDomain L517
structure RecognitionCostSystem L521
def canonicalSigma L530
def canonicalRecognitionCostSystem L534
theorem canonicalRecognitionCostSystem_domain L543
theorem canonicalRecognitionCostSystem_cost_one L547
theorem canonicalRecognitionCostSystem_cost_inv L552
def seqShift L559
def windowSums L562
theorem windowSums_shift_equivariant L567
structure CostAlgebraData L589
def canonicalCostAlgebra L602
theorem cost_algebra_unique L612
theorem cost_algebra_unique_aczel L641
structure CostMorphism L655
def reciprocalAuto L688
theorem reciprocal_involution L691
theorem reciprocal_preserves_cost L697
theorem J_eq_iff_eq_or_inv L704
abbrev PosReal L732
def posMul L735
def posInv L739
def posOne L743
def posTwo L744
def posHalf L745
theorem posInv_inv L747
theorem posInv_one L751
theorem posInv_two L755
theorem posInv_half L759
def JAut L764
theorem multiplicative L774
theorem preserves_cost L779
theorem ext L783
def id L789
def reciprocal L798
def comp L808

… and 14 more