cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single Berry-phase certificate: the cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the structural Berry-curvature claim Omega ~ J(phi) a^2 can point here for the certificate object. The body is a pure structure instance wiring three sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and the canonical threshold $T$ obeys $T>0$.
background
The module treats Berry curvature in topological materials as a structural consequence of the Recognition Science J-cost: $\Omega(k)\sim J(\varphi),a^2$ with lattice constant $a$, giving the numerical scale $\Omega\approx 1.06\times 10^{-20},\mathrm{m}^2$. Status is structural (zero sorry, zero axiom).
The certificate structure Berry4v2Cert bundles three Prop fields about a domain cost $C(m,e)$ (built from the RS cost $J$) and a positive canonical threshold. The first field forces vanishing cost when the two arguments coincide; the second is nonnegativity for positive arguments; the third is positivity of the threshold used as a creation or detection cutoff (linked to the Berry threshold scale $\varphi^{-1}$ in the broader framework).
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The three field proofs live as sibling lemmas in this module and are simply assembled here.
proof idea
Pure structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional tactic work; the definition is the instance itself.
why it matters
Gives a single named inhabitant of the Berry-phase v2 certificate so downstream physics lemmas can assume one object rather than three separate hypotheses. The module frames this as the structural backbone for $\Omega=J(\varphi),a^2$, tying Berry curvature to the forced J-cost (T5) and the golden-ratio fixed point $\varphi$ (T6). No used-by edges are recorded yet; the natural consumer is any theorem that needs the packaged certificate (for example inhabitance or a curvature-scale derivation). Closes the local packaging step of the Plan v7 Berry pass without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.