module module high

`IndisputableMonolith.Algebra.CostAlgebra`

The Algebra.CostAlgebra module defines the J-cost function as the explicit solution to the Recognition Composition Law. Researchers tracing the T5 uniqueness step in the forcing chain cite this module for the closed form and its algebraic properties. The module assembles definitions and lemmas from the imported FunctionalEquation files to establish RCL satisfaction and basic 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 layer of Recognition Science and supplies the concrete J-cost that satisfies the Recognition Composition Law. It imports the Cost module together with FunctionalEquation, whose doc states it supplies lemmas for the T5 cost uniqueness proof, and the Aczel compatibility layer for legacy closures. The sibling declarations introduce J, J_at_one, J_reciprocal, J_nonneg, J_defect_form, SatisfiesRCL, RCL_holds, and the costCompose family that encodes the law under multiplication and division.

proof idea

This is a definition module, no proofs. It collects the J definition from the module doc-comment and states the RCL satisfaction and composition lemmas that follow from the upstream FunctionalEquation results.

why it matters in Recognition Science

The module supplies the algebraic core for the J-cost that PhiRing and RecognitionCategory import and extend. It realizes the T5 J-uniqueness landmark of the forcing chain by giving the explicit form used downstream for the phi-ladder and recognition structures.

scope and limits

Does not contain the full T5 uniqueness proof.
Does not derive physical constants or the phi-ladder.
Does not address the eight-tick octave or D=3.
Does not import UnifiedForcingChain.

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