ConfigSpaceD3Cert
plain-language theorem explainer
Certificate structure packaging three metric axioms for the D=3 recognition configuration space: diagonal domain-cost vanishes, domain-cost is nonnegative on positive arguments, and the canonical threshold is positive. Anyone citing the inhabited D=3 config-space certificate uses this bundle. It is a pure structure definition with no proof body; inhabitants discharge the three fields separately.
Claim. A D=3 configuration-space 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 fixes the Recognition Science configuration space at spatial dimension three: $C_3=\mathbb{R}^3$ equipped with the recognition metric. That metric is the J-cost Riemannian form $ds^2=J(dx/x)$ on the positive orthant, required to be positive definite for all $x>0$. Status is structural (no sorry, no axioms).
Domain cost is the local cost functional on pairs of reals that underlies the metric comparison; the diagonal-vanishing and nonnegativity fields are the elementary positivity axioms one needs before promoting it to a Riemannian structure. The canonical threshold is the positive scale cut used to separate admissible configurations from the zero section.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states. The present certificate lifts that style of positivity statement to the domain-cost pair used by the D=3 geometry.
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity of domain cost on the positive quadrant, positivity of the canonical threshold). Downstream, the concrete inhabitant cert fills them by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Packages the minimal positivity and normalization data for the D=3 recognition configuration space so later geometry can cite one object rather than three scattered lemmas. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty ConfigSpaceD3Cert, closing the structural certificate for the module.
In the forcing chain this sits under T8 (D=3 spatial dimensions): once dimension is forced, the configuration space must carry a well-behaved J-cost metric on the positive orthant. The certificate is the Lean-side checklist that those metric seeds hold. It does not itself derive D=3; it records the cost axioms the D=3 geometry consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.