ConfigDimD3_v3Cert
plain-language theorem explainer
Certificate structure that packages three elementary cost and threshold properties used by the D=3 configuration-dimension argument. Anyone citing the ConfigDim D3 v3 structural theorem (eight-tick closure forces spatial dimension three) depends on this bundle. It is a pure structure definition: three Prop fields, no proof body.
Claim. A D=3 configuration certificate is a triple of properties: (i) domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ whenever $r\neq 0$; (ii) domain cost is nonnegative for positive mass and energy arguments, $0<m$, $0<e\Rightarrow 0\le\mathrm{domainCost}(m,e)$; (iii) the canonical threshold is strictly positive, $0<\tau_{\mathrm{can}}$.
background
The module proves spatial dimension $D=3$ from eight-tick closure: the recognition cycle has period $8=2^3$, so it closes after exactly three binary recursions. That is the unique $D$ for which the recognition lattice is minimal and self-similar (framework landmark T8).
Domain cost is the real-valued cost assigned to a mass-energy pair in the configuration argument. The first field requires it to vanish when the two arguments coincide (identity events sit at the J-cost minimum). The second requires nonnegativity for positive inputs, matching the upstream fact that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The third field asserts positivity of the canonical threshold that separates admissible from inadmissible configurations.
These three Props are the interface the rest of the module inhabits; they do not themselves encode the $2^3$ counting argument.
proof idea
No proof body: this is a structure declaration. The three fields are bare propositions. Downstream, cert fills them by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that inhabitant to obtain Nonempty.
why it matters
This certificate is the typed interface for the ConfigDim D3 v3 structural theorem (module status: 0 sorry, 0 axiom). Downstream cert and cert_inhabited discharge inhabitance, so later arguments can assume the three cost/threshold facts without re-proving them. In the Recognition forcing chain it sits under T8 ($D=3$ spatial dimensions forced by eight-tick octave period $2^3$). It does not re-derive T5 J-uniqueness or T7 eight-tick existence; it only packages the cost side-conditions those steps need when specialized to configuration dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.