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 the geometry of cost functions in log-coordinates cite these objects when working with the weighted aggregate dot product. The module supplies definitions together with basic algebraic closure properties of the sets.
claimLet $H$ denote the rank-one Hessian of the cost depending only on the aggregate $\dot{\alpha} t$. The radical distribution consists of the set $\mathrm{Radical} = \{v \mid H(v) = 0\}$ and the level sets $\mathrm{LevelSet}_c = \{v \mid H(v) = c\}$, together with the affine shift map.
background
The imported Hessian module states that in log-coordinates the n-dimensional reciprocal cost depends only on the single weighted aggregate $\mathrm{dot},\alpha, t$, so its Hessian is rank-one. This module therefore introduces the radical distribution of that metric. Sibling definitions supply the concrete sets Radical and LevelSet, the affineShift operator, and the membership and closure lemmas (zero_mem_Radical, add_mem_Radical, smul_mem_Radical, 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 that completes the public Hessian interface referenced by Metric.lean. It therefore feeds the cost geometry used in the Recognition Science n-dimensional cost model and the rank-one structure that follows from the single aggregate dependence.
scope and limits
- Does not prove any theorems.
- Does not import modules beyond Hessian.
- Does not define the Hessian metric itself.
- Does not treat non-rank-one cases.
depends on (1)
declarations in this module (14)
-
def
Radical -
def
LevelSet -
def
affineShift -
theorem
mem_Radical_iff -
theorem
mem_LevelSet_iff -
theorem
zero_mem_Radical -
theorem
add_mem_Radical -
theorem
smul_mem_Radical -
theorem
sub_mem_Radical -
theorem
quadraticHessian_eq_zero_iff -
theorem
dot_affineShift -
theorem
affineShift_mem_LevelSet -
theorem
radical_integrable_by_affine_leaves -
theorem
preserves_own_leaf_iff_mem_Radical