RSPhysics008Cert
plain-language theorem explainer
Certificate bundle for Physics Module 8: the domain cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Anyone citing the structural Strong-CP / θ=0 claim from eight-tick uniqueness will point here. It is a plain structure packing three already-proved field lemmas; no new proof work lives in the declaration itself.
Claim. A certificate consists of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is non-negative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 8 targets the Strong CP problem: QCD θ = 0 is forced by eight-tick uniqueness rather than by a dynamical axion. The module is marked structural (zero sorry, zero axiom).
The domain cost is the local cost functional on pairs of positive reals (mass-like and energy-like coordinates) used in this module. Its diagonal vanishing and non-negativity mirror the global J-cost story: recognition cost is minimized at identity and never goes negative. Upstream, ObserverForcing already records that every recognition event has non-negative cost via Jcost_nonneg.
The canonical threshold is the positive cutoff against which domain-cost comparisons are made when the module argues that the CP-odd phase is forced to zero under the eight-tick (period $2^3$) constraint from the forcing chain (T7).
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued obligations. Downstream, the concrete inhabitant cert fills them by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Inhabitation is then immediate: cert_inhabited wraps that single value in Nonempty.
why it matters
Module 8's structural claim is that eight-tick uniqueness forces QCD θ = 0, solving Strong CP without an axion. This certificate is the typed interface those lemmas must satisfy before the module can export a clean witness.
Downstream, cert is the canonical inhabitant and cert_inhabited proves the type is nonempty. That nonempty witness is what later physics exports can depend on when they cite the θ = 0 structural theorem. Framework landmarks in play are T7 (eight-tick octave) and the non-negativity of recognition cost inherited from the J-cost calculus (T5 / RCL lineage).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.