cert
plain-language theorem explainer
Packages the three structural facts needed for the FDM filament-fusion certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Materials theorists citing the J-cost bond-fraction story use this as the inhabited certificate object. Construction is a three-field structure instance wiring existing lemmas.
Claim. There is a certificate consisting of: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical fusion threshold is strictly positive.
background
The module treats FDM interlayer bond strength as a Recognition-Science cost problem. Ideal layer bonding is tied to the fraction $1 - J(\varphi) \approx 88.2%$, while a poor print is modeled by a void fraction $J(\varphi)^2 \approx 1.4%$, giving residual strength in the $80$–$85%$ band. Here $J$ is the unique nonnegative cost $J(x) = (x + x^{-1})/2 - 1$ forced by the Recognition Composition Law (T5).
Domain cost is the local cost functional on matched versus exposed filament scales; it is required to vanish when the two arguments agree and to stay nonnegative when both are positive. The canonical threshold is the positive cutoff used to decide whether a bond event is accepted. Upstream, nonnegativity of recognition cost is already known: every recognition event has cost $\ge 0$ because $J$ itself is nonnegative on the positive reals.
proof idea
One-line structure instance. The three fields of FuseFilament3Cert are filled by the sibling lemmas that already prove diagonal vanishing of domain cost, nonnegativity of domain cost for positive arguments, and positivity of the canonical threshold. No extra algebra is performed at this site.
why it matters
Gives an inhabited certificate object for the structural FDM-from-J-cost theorem (module status: 0 sorry, 0 axiom). Downstream consumers can assume a single package rather than three separate hypotheses when deriving bond-fraction or void-fraction claims from $J$. The construction sits in the materials layer that translates the forced cost $J$ and the golden-ratio fixed point $\varphi$ into a printable interlayer strength prediction. No parent theorems currently depend on it in the graph, so it is the terminal certificate for this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.