NNOverparamCert
plain-language theorem explainer
Certificate structure bundling three analytic facts about the domain cost and the canonical overparameterization threshold. Anyone citing the RS claim that the optimal parameters/data ratio is J(φ)^{-1} ≈ 8.47 times the minimum will need an inhabitant of this type. It is a pure structure definition; the concrete witness is assembled from the sibling lemmas on diagonal vanishing, nonnegativity, and threshold positivity.
Claim. A neural-network overparameterization certificate is a triple of facts: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for every $r\neq 0$; (ii) the domain cost is nonnegative on positive scales, $0\le\mathrm{cost}(m,e)$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module derives the classical neural-network overparameterization heuristic (parameters/data roughly 5–10× for generalization) from the Recognition Science J-cost. In RS units the optimal ratio is forced to $J(\varphi)^{-1}\approx 8.47$ times the minimum parameter count, where $J(x)=(x+x^{-1})/2-1$ is the unique cost fixed by the Recognition Composition Law and $\varphi$ is the self-similar fixed point (forcing steps T5–T6).
The domain cost is the two-argument specialization of that J-cost used to compare a model scale $m$ against a data/evidence scale $e$. Upstream, cost_nonneg already records that every recognition event has nonnegative cost, via $J\ge 0$ on the positive reals. The present structure simply packages the three elementary properties of the domain cost and of the derived canonical threshold that later theorems treat as a single certificate object.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). An inhabitant is supplied downstream by the definition cert, which plugs in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
This certificate is the typed interface for the whole Materials.TrainedNeuralNetworkFromJCost development. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty NNOverparamCert, closing the structural theorem (0 sorry, 0 axiom) announced in the module header.
In the broader RS chain the object sits under the J-uniqueness and $\varphi$-forcing landmarks (T5–T6): once $J$ and $\varphi$ are fixed, the overparameterization ratio $J(\varphi)^{-1}$ is a pure number, and the certificate isolates exactly the cost inequalities needed to treat that number as a recognition budget rather than an empirical fit. It does not itself compute the numerical factor; it guarantees the analytic hypotheses under which that factor is meaningful.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.