FuseFilament3Cert
plain-language theorem explainer
Certificate structure packaging three analytic facts for FDM interlayer bond strength from J-cost: diagonal vanishing of domain cost, non-negativity for positive arguments, and positivity of the canonical threshold. Materials work citing the RS bond-fraction claim (ideal layer bonding at 1-J(φ)) references this bundle. Pure structure definition; no proof body.
Claim. A fuse-filament certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats FDM (fused deposition modeling) interlayer bond strength as a Recognition Science materials claim. Ideal layer bonding is identified with the bond fraction $1-J(\varphi)\approx 88.2%$, while a poor print is tied to a void fraction $J(\varphi)^2\approx 1.4%$ and residual strength in the $80$–$85%$ band. Status is structural: zero sorry, zero axioms.
Domain cost is the materials-side cost functional (imported from the Cost layer and Constants) evaluated on a pair of positive reals; the certificate demands it vanish on the diagonal and stay nonnegative off it. The canonical threshold is the positive cutoff used to separate bonded from under-bonded regimes. Upstream, recognition-event cost is already known to be nonnegative via $J$-cost nonnegativity on positive states (cost_nonneg in ObserverForcing).
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing, nonnegativity for positive arguments, threshold positivity). Inhabitation is deferred to the sibling cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named interface for the analytic hypotheses the FDM-from-J-cost argument needs, so downstream lemmas can depend on one certificate rather than three scattered facts. Immediate consumers are cert (the concrete inhabitant wiring the three sibling lemmas) and cert_inhabited (Nonempty of the structure). In the broader RS chain this sits under materials applications of T5 J-uniqueness and the Recognition Composition Law: bond fraction is read off $1-J(\varphi)$ with $\varphi$ the self-similar fixed point from T6. It closes the structural packaging for the Plan v7 FDM strength claim without adding physics axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.