HydrogenSpect3Cert
plain-language theorem explainer
Certificate bundling three analytic side-conditions used to derive Balmer-line ratios from the Recognition J-cost: diagonal domain cost vanishes, cost is nonnegative for positive mass and energy, and the canonical threshold is positive. Anyone citing the inhabited hydrogen-spectrum certificate or the concrete cert instance needs this bundle. Pure structure definition; no proof body.
Claim. A hydrogen-spectrum certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module derives hydrogen emission lines (Balmer $H_\alpha,H_\beta,H_\gamma$) from the phi-ladder and the Recognition J-cost. Adjacent Balmer wavelengths are claimed to differ by a factor near $\varphi^{0.8}$. Status is structural: zero sorry, zero axiom.
Domain cost is the local cost functional on mass/energy pairs that the spectrum argument uses in place of a raw recognition event. It inherits nonnegativity from the upstream fact that every recognition event has nonnegative cost (via $J$-cost nonnegativity at positive state). The canonical threshold is the positive cutoff against which spectral steps are compared.
The certificate packages exactly the three side-conditions the later inhabited instance must discharge: vanishing on the diagonal, nonnegativity off-axis for positive parameters, and a strictly positive threshold.
proof idea
No proof: this is a structure whose three fields are propositions. Downstream, cert fills the fields by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that instance as Nonempty.
why it matters
Gives a single named interface for the analytic hypotheses of the hydrogen-spectrum-from-J-cost structural theorem. Downstream cert inhabits it and cert_inhabited records nonemptiness, so later spectrum arguments can assume one object rather than three free-floating lemmas.
Sits in the Foundation layer that connects the forcing chain (T5 J-uniqueness, T6 $\varphi$ fixed point) to spectroscopic observables on the phi-ladder. The module framing is Balmer ratios near $\varphi^{0.8}$; this certificate does not itself compute wavelengths, but it is the gate that makes the cost-based derivation well-typed and nonnegative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.