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 building the phi-ring and recognition category structures cite this module for the cost algebra primitives. The module assembles definitions and basic lemmas from imported functional equation results to verify the composition law and related identities.

claim$J(x) = \frac12(x + x^{-1}) - 1$ satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.

background

This module sits in the Algebra domain and imports Cost along with FunctionalEquation helpers for the T5 cost uniqueness proof. The J-cost is introduced as the unique cost satisfying the Recognition Composition Law (RCL). Upstream, FunctionalEquation supplies lemmas for T5, while FunctionalEquationAczel isolates Aczél-based closure theorems for compatibility with callers needing one-line results.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

CostAlgebra supplies the algebraic foundation for J that is imported by PhiRing and RecognitionCategory. It fills the T5 step in the forcing chain by providing the cost function used in subsequent constructions of the phi-ring and recognition structures.

scope and limits

Does not establish uniqueness of J without the imported functional equation lemmas.
Does not connect J to physical constants such as alpha or G.
Does not address the phi-ladder or mass formula.
Does not include proofs of the RCL itself.

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