module module high

`IndisputableMonolith.Foundation.JCostGeometry`

JCostGeometry develops algebraic and geometric properties of the J-cost function in the Recognition Science foundation layer. It establishes identities such as J(1) = 0, non-negativity, zero only at unity, reciprocity, and squared-form relations that support cost geometry. Foundation researchers cite these when building topological veto arguments and dimensional constraints. The module proceeds by direct algebraic verification of each listed property extending the core definition.

claimThe J-cost function $J(x) = (x + x^{-1})/2 - 1$ satisfies $J(1) = 0$, $J(x) = J(x^{-1})$, $J(x) > 0$ for $x > 0$ with $x$ away from 1, the squared identity $J(x)^2 = J(x^2) + 2J(x)$, and related ratio and total-cost forms; totalJcost and geometricMean are defined as the natural sum and mean over configurations.

background

The module imports the core J-cost definition from JcostCore, where J satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). It introduces totalJcost as the sum of J-values over a configuration and geometricMean derived from it. The local setting is the foundation layer of Recognition Science, where J-cost quantifies multiplicative deviation from unity and feeds the forcing chain from T5 J-uniqueness through T8 D = 3.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the J-cost geometry required by the TopologicalVeto module for proving integer linking invariants exist only in D = 3. It fills foundation paper F1.1.2 on J(1) = 0 and extends to the geometric identities needed for the eight-tick octave and spatial-dimension forcing.

scope and limits

Does not treat J-cost for non-positive arguments.
Does not incorporate quantum or higher-order corrections.
Does not prove the full T0-T8 forcing chain.
Does not address applications outside topological veto.

used by (1)

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

IndisputableMonolith.Foundation.TopologicalVeto module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (23)

theorem jcost_at_one L36
theorem jcost_nonneg' L39
theorem jcost_eq_zero_iff L42
theorem jcost_reciprocal L58
theorem jcost_pos_away_from_one L63
theorem jcost_unit_curvature L68
theorem jcost_exp_eq L74
theorem jcost_squared_form L79
theorem jcost_ratio_zero_iff L85
def totalJcost L92
theorem totalJcost_nonneg L96
def geometricMean L109
theorem geometricMean_pos L113
theorem totalJcost_at_geomean_symmetric L121
def arithmeticMean L157
theorem geometric_ne_arithmetic L161
theorem simultaneous_differs_from_sequential L182
theorem rcl_identity L190
def phi L199
theorem phi_sq L202
theorem phi_pos L209
def jBit L215
theorem jBit_pos L218