module module high

`IndisputableMonolith.Algebra.CostAlgebra`

CostAlgebra defines the J-cost function as the unique solution to the Recognition Composition Law with explicit form J(x) = (x + x^{-1})/2 - 1. Algebraists extending Recognition Science to ring and category structures cite the module as the base algebraic layer. It organizes imported lemmas from Cost and FunctionalEquation into a coherent package of definitions and basic properties.

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)$.

background

The module lives in the Algebra domain and imports the core Cost definitions together with the T5 uniqueness helpers in FunctionalEquation and the Aczél compatibility layer. It introduces J as the cost function obeying the Recognition Composition Law, plus supporting facts such as J_at_one, J_reciprocal, J_nonneg, J_defect_form, SatisfiesRCL, and RCL_holds. The local setting is the derivation of all physics from a single functional equation, where J realizes the T5 uniqueness step in the forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module is imported by PhiRing and RecognitionCategory, supplying the J-cost foundation those constructions require. It directly encodes the T5 J-uniqueness landmark (J(x) = (x + x^{-1})/2 - 1) from the forcing chain and the Recognition Composition Law.

scope and limits

Does not contain the uniqueness proof for J.
Does not derive numerical constants or mass formulas.
Does not address extensions beyond the base RCL algebra.

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