module module high

`IndisputableMonolith.Foundation.JCostGeometry`

JCostGeometry module collects basic algebraic properties of the J-cost function J(x) = (x + x^{-1})/2 - 1, starting from J(1) = 0. Researchers building Recognition Science foundations cite it for cost calculations ahead of topological arguments. The module consists of direct lemmas derived from the JcostCore definition.

claim$J(1) = 0$, $J(x) \geq 0$ for $x > 0$, $J(x) = J(x^{-1})$, and related identities such as the squared form and ratio conditions.

background

The module builds directly on the J-cost definition imported from IndisputableMonolith.Cost.JcostCore. It introduces no new core objects but records geometric consequences of the J function, including non-negativity and reciprocity. The local theoretical setting is the early foundation layer (F1.1.2) that supplies cost identities before any topological or dimensional results.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies J-cost identities to the TopologicalVeto module, which establishes the topological capacity veto in D = 3 and the existence of the integer linking invariant only in three dimensions. It fills the F1.1.2 slot in the foundation chain that precedes F6.

scope and limits

Does not define the J function or the Recognition Composition Law.
Does not treat the phi-ladder, mass formulas, or Berry threshold.
Does not address spatial dimensions or Alexander duality.
Does not contain any topological or physical applications.

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