module module moderate

`IndisputableMonolith.Cost.Ndim.RadicalDistribution`

The RadicalDistribution module defines the radical and associated level sets of the rank-one Hessian metric for the n-dimensional reciprocal cost. Researchers analyzing metric degeneracy in log-coordinates within the Recognition Science cost framework would cite these definitions. The module supplies the core objects Radical and LevelSet together with their basic algebraic properties.

claimLet $H$ denote the rank-one Hessian of the cost depending only on the aggregate $oldsymbol{eta}oldsymbol{ au}$. The radical distribution is the subspace $\{v\mid H(v,w)=0\ \forall w\}$ equipped with its level sets and affine shifts.

background

The module imports IndisputableMonolith.Cost.Ndim.Hessian, whose doc-comment states that in log-coordinates the n-dimensional cost depends only on the single weighted aggregate dot α t, so its Hessian is rank-one. This supplies the setting for the radical (kernel) of that quadratic form. Sibling definitions introduce Radical as the radical subspace, LevelSet as the associated level sets, affineShift, and closure properties such as zero_mem_Radical, add_mem_Radical and smul_mem_Radical.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the radical distribution of the rank-one Hessian metric, providing the algebraic substrate for cost and metric constructions that depend on the Hessian module. It fills the structural gap between the rank-one reduction and higher-level distribution properties in the Ndim cost layer.

scope and limits

Does not derive the explicit matrix entries of the Hessian.
Does not relate the radical to the J-function or the Recognition Composition Law.
Does not contain numerical evaluations or dimension-specific computations.

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