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)
depends on (3)
declarations in this module (94)
-
def
J -
theorem
J_at_one -
theorem
J_reciprocal -
theorem
J_nonneg -
theorem
J_defect_form -
def
SatisfiesRCL -
theorem
RCL_holds -
def
costCompose -
theorem
costCompose_comm -
theorem
costCompose_assoc_defect -
theorem
costCompose_flexible -
theorem
costCompose_zero_left -
theorem
costCompose_zero_right -
theorem
costCompose_nonneg -
theorem
costCompose_factored -
theorem
costCompose_no_identity -
theorem
costCompose_power_assoc -
theorem
costCompose_fourfold_power_counterexample -
def
H -
theorem
H_at_one -
theorem
H_dAlembert -
abbrev
ShiftedCarrier -
def
shiftedCompose -
def
shiftedUnit -
theorem
shiftedUnit_val -
theorem
shiftedCompose_val -
theorem
H_ge_one -
def
shiftedOfH -
abbrev
ShiftedHValue -
def
shiftedComposeH -
theorem
shiftedComposeH_val -
def
shiftedHValueOf -
def
defectDist -
theorem
defectDist_self -
theorem
defectDist_symm -
theorem
defectDist_nonneg -
theorem
J_le_J_of_inv_le_le -
theorem
defectDist_le_J_of_ratio_bounds -
theorem
quasiTriangleConstant_eq -
theorem
defectDist_quasi_triangle_local -
theorem
defectDist_no_global_quasi_triangle -
theorem
costCompose_sub_left -
theorem
costCompose_left_cancel -
theorem
costCompose_right_cancel -
def
PositiveDomain -
structure
RecognitionCostSystem -
def
canonicalSigma -
def
canonicalRecognitionCostSystem -
theorem
canonicalRecognitionCostSystem_domain -
theorem
canonicalRecognitionCostSystem_cost_one -
theorem
canonicalRecognitionCostSystem_cost_inv -
def
seqShift -
def
windowSums -
theorem
windowSums_shift_equivariant -
structure
CostAlgebraData -
def
canonicalCostAlgebra -
theorem
cost_algebra_unique -
theorem
cost_algebra_unique_aczel -
structure
CostMorphism -
def
reciprocalAuto -
theorem
reciprocal_involution -
theorem
reciprocal_preserves_cost -
theorem
J_eq_iff_eq_or_inv -
abbrev
PosReal -
def
posMul -
def
posInv -
def
posOne -
def
posTwo -
def
posHalf -
theorem
posInv_inv -
theorem
posInv_one -
theorem
posInv_two -
theorem
posInv_half -
def
JAut -
theorem
multiplicative -
theorem
preserves_cost -
theorem
ext -
def
id -
def
reciprocal -
def
comp