module module moderate

`IndisputableMonolith.Cost.Ndim.RadicalDistribution`

The RadicalDistribution module defines the radical and level-set structures for the rank-one Hessian metric arising in n-dimensional reciprocal costs. Researchers extending the cost framework in Recognition Science cite it when working with affine shifts and membership conditions on those sets. It consists entirely of definitions and basic lemmas that import the Hessian module and expose Radical, LevelSet, and affineShift.

claimThe radical distribution of the rank-one Hessian metric on the n-dimensional reciprocal cost, together with its level sets and affine shifts.

background

The upstream Hessian module supplies formulas for the n-dimensional reciprocal cost. Its doc-comment states that in log-coordinates the cost depends only on the single weighted aggregate dot α t, so its Hessian is rank-one. The present module introduces the radical distribution to encode that rank-one structure explicitly. It also defines LevelSet and affineShift together with the membership lemmas mem_Radical_iff, zero_mem_Radical, add_mem_Radical, and quadraticHessian_eq_zero_iff.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the radical distribution required by the n-dimensional cost layer in Recognition Science. It directly extends the Hessian formulas for the reciprocal cost and prepares the structures used in higher-level cost calculations, even though the current used_by list is empty.

scope and limits

Does not compute eigenvalues or trace of the Hessian.
Does not treat perturbations that raise the Hessian rank.
Does not connect to the forcing chain T0-T8 or the Recognition Composition Law.
Does not supply numerical values for constants such as alpha or phi.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.Ndim.Hessian module_import

declarations in this module (14)

def Radical L20
def LevelSet L24
def affineShift L28
theorem mem_Radical_iff L31
theorem mem_LevelSet_iff L34
theorem zero_mem_Radical L37
theorem add_mem_Radical L42
theorem smul_mem_Radical L54
theorem sub_mem_Radical L67
theorem quadraticHessian_eq_zero_iff L74
theorem dot_affineShift L90
theorem affineShift_mem_LevelSet L103
theorem radical_integrable_by_affine_leaves L113
theorem preserves_own_leaf_iff_mem_Radical L121