Gap45ExactV2Cert
plain-language theorem explainer
Certificate structure bundling three analytic facts used by the exact gap-45 (v2) development: diagonal domain-cost vanishes off zero, domain-cost is nonnegative on the positive quadrant, and the canonical threshold is positive. Anyone citing the inhabited gap-45 certificate reaches this type. Pure definitional packaging; the proofs live in the field witnesses.
Claim. A gap-45 exact certificate is a triple of statements: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all reals $m>0$ and $e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats gap-45 as the exact integer $45 = D^2(D+2) = 9\cdot 5$ forced by spatial dimension $D=3$ (forcing landmark T8). The same integer appears as a classical angle ($\pi/4$), a mechanical optimum, and related counting identities; the development claims a structural theorem with no sorry and no axioms.
Domain cost is the local cost functional on pairs of positive reals (measure/energy style arguments) used inside this gap-45 layer. The first field asks that cost vanish on the diagonal away from zero; the second asks nonnegativity on the open positive quadrant. The canonical threshold is the positive cutoff against which gap-45 comparisons are made.
Upstream, recognition-event cost is already known nonnegative via the J-cost minimum at identity (cost_nonneg in ObserverForcing: "The cost of any recognition event is non-negative"). The present structure lifts that nonnegativity pattern to the domain-cost interface used by gap-45.
proof idea
No proof body: this is a structure declaration. It only names three Prop fields. Inhabitation is deferred to the sibling cert, which assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to those fields, and to cert_inhabited, which packages ⟨cert⟩ as Nonempty.
why it matters
Gives a single named type for the analytic hypotheses the gap-45 exact (v2) layer needs, so downstream lemmas can depend on one certificate rather than three loose facts. Immediate consumers are cert (the concrete witness) and cert_inhabited (nonemptiness). That closes the structural packaging for the module claim "gap-45 = 45 = D^2(D+2) = 9*5" forced from $D=3$, aligning with T8 in the forcing chain. It does not itself compute the integer 45; it only standardizes the cost/threshold side conditions the exact argument uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.