cert
plain-language theorem explainer
assembles the three algebraic side-conditions that certify the RS superhydrophobicity model: vanishing domain cost on the diagonal, non-negativity of domain cost for positive arguments, and positivity of the canonical threshold. Materials theorists citing the phi-ladder contact-angle story use it as the packaged witness. The body is a pure structure constructor wiring three already-proved sibling lemmas.
Claim. There is a superhydrophobicity certificate: the domain cost vanishes on equal nonzero arguments ($\mathrm{domainCost}(r,r)=0$ for $r\neq 0$), is nonnegative for positive mass and energy arguments, and the canonical threshold is strictly positive.
background
The module treats superhydrophobicity (contact angle above roughly $150^\circ$) as a Recognition Science materials claim. The module doc notes the rough match $150 \approx 180,(1-J(\varphi))$, tying the angle threshold to the unique J-cost fixed by the forcing chain (T5) and the golden ratio $\varphi$ (T6).
domainCost is the local cost functional on mass/energy pairs used in this wettability model; the certificate demands it behave like a genuine cost (zero on the diagonal, nonnegative off it). canonicalThreshold is the positive cutoff that separates the superhydrophobic regime.
Upstream, non-negativity of recognition cost is already forced in ObserverForcing via $J$-cost non-negativity. The structure SuperhydrophobicityCert packages exactly the three Prop fields that a downstream materials argument may assume without reopening the cost calculus.
proof idea
One-line structure inhabitation. The three fields of SuperhydrophobicityCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new arithmetic is performed; the definition is the witness bundle.
why it matters
Gives a zero-sorry, zero-axiom certificate object for the Plan v7 superhydrophobicity pass in the materials layer. It sits at the interface between the abstract J-cost (T5 uniqueness, RCL) and a concrete surface-physics claim: contact angles past $\sim 150^\circ$ as a phi-ladder threshold phenomenon. No downstream consumers are recorded yet; the natural parent is any theorem that assumes a SuperhydrophobicityCert to derive angle or energy bounds. Closes the structural side of the module status line (0 sorry, 0 axiom) by exhibiting an inhabited certificate rather than leaving the structure abstract.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.