cert_inhabited
plain-language theorem explainer
The Module 6 structural certificate is inhabited: a witness exists packing diagonal vanishing of the domain cost, its nonnegativity on positive mass-energy, and positivity of the canonical threshold. Anyone exporting the Higgs-VEV structural pack cites this inhabitance fact. The proof is a one-line term that wraps the already-assembled certificate record.
Claim. The set of Module 6 certificates is nonempty: there exists a record packing (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$, (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$, and (iii) the canonical threshold is strictly positive.
background
Physics Module 6 records the structural comparison of the Higgs vacuum expectation value ratio $v/M_Z\approx 246/91.2=2.70$ against $\varphi^2\approx 2.618$ (about 3 percent off). The module is marked as a structural theorem: zero sorry, zero axioms.
The certificate structure bundles three elementary properties of the local domain cost (imported from the Cost layer) and a canonical threshold: the cost vanishes on the diagonal for nonzero arguments, stays nonnegative on the positive quadrant, and the threshold is positive. These are the only obligations the inhabitance theorem discharges.
Upstream, the certificate type is just the product of those three propositions; the concrete record that fills them is built earlier in the same module from the corresponding lemmas on domain cost and the threshold.
proof idea
Pure term proof. The goal is Nonempty of the certificate structure. The term is the anonymous constructor applied to the preexisting certificate record, which already holds proofs of diagonal vanishing, nonnegativity, and threshold positivity. No tactics, no further lemmas.
why it matters
Gives the exportable inhabitance witness for the Module 6 structural pack. The module sits in the physics layer that compares the observed Higgs ratio to $\varphi^2$, the self-similar fixed point forced at T6 of the unified forcing chain. No downstream consumers are wired yet; the theorem simply guarantees that the certificate type is realized, so later assembly or audit code can assume a concrete witness without rebuilding the three field proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.