PolyEntangleCert
plain-language theorem explainer
A certificate packing three structural properties of the polymer-domain cost: diagonal vanishing, non-negativity for positive monomer and entanglement scales, and a strictly positive canonical threshold. Materials and RS polymer models cite it to pin the entanglement-length formula Ne ~ J(φ)^{-2} × backbone. The object is a pure structure; inhabitants are assembled from sibling lemmas.
Claim. A polymer-entanglement certificate is a record of three facts: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module derives polymer entanglement density from the Recognition Science J-cost. Empirically, entanglement length $N_e$ sits in the 100–1000 monomer band; RS predicts $N_e = J(\varphi)^{-2}\times\mathrm{backbone_count}\approx 71.7\times\mathrm{backbone}$, giving $N_e=358$ for backbone 5, consistent with many systems.
Domain cost is the local cost functional on monomer and entanglement scales; the certificate demands it vanish when the two arguments coincide (identity recognition) and stay non-negative off the axes. The canonical threshold is the positive cutoff used to mark the entanglement regime.
Upstream, non-negativity of recognition cost is already forced: any recognition event has cost $\ge 0$ via $J$-cost non-negativity on positive states. The certificate lifts that global fact into the polymer-domain signature.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Downstream, cert fills them by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then packages that witness as Nonempty.
why it matters
Gives a single named bundle for the structural hypotheses of the polymer-entanglement story in the Materials layer (Plan v7, 107th pass). Downstream cert and cert_inhabited show the bundle is realized with zero sorry, so the entanglement-length claim sits on a closed certificate rather than ad-hoc assumptions.
It ties materials phenomenology to the J-cost minimum and non-negativity forced in the foundation (ObserverForcing / PRC), and to the self-similar scale $\varphi$ that appears in $J(\varphi)^{-2}$. It does not itself compute $N_e$; it certifies the cost and threshold scaffolding that make that formula well-posed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.