RSFDNStructural005Cert
plain-language theorem explainer
Certificate structure bundling three structural facts for the eight-tick foundation: domain cost vanishes on equal nonzero arguments, is nonnegative for positive measure and energy, and the canonical threshold is strictly positive. Downstream code cites it via the concrete cert instance and the Nonempty inhabitation theorem. Pure structure definition with no proof body.
Claim. A certificate packing three claims: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_005 records structural facts for the Recognition Science eight-tick: one full traversal of the binary recognition lattice has period $2^D = 8$ (the T7 octave). Status is structural theorem material with no sorry and no axioms.
Domain cost is the real-valued cost assigned to a pair of positive scale parameters (measure and energy style arguments). The diagonal vanishing condition says equal nonzero arguments incur zero cost, matching the J-cost minimum at identity. Nonnegativity of domain cost is the continuous analogue of the upstream fact that every recognition event has nonnegative cost (via J-cost nonnegativity). The canonical threshold is the positive cutoff used to separate trivial from nontrivial recognition steps in this structural layer.
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is supplied later by the concrete cert value, which fills the fields from the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named bundle for the three structural obligations of foundation module 5 so downstream code can demand or inhabit one object rather than three loose lemmas. The parent definitions are the concrete cert instance and cert_inhabited (Nonempty of this structure), which close the module as a zero-sorry structural theorem.
In the forcing chain this sits under the eight-tick octave (T7, period $2^3$) and the D = 3 spatial forcing (T8): a complete binary lattice traversal is the discrete skeleton on which cost and threshold statements are stated. It does not itself force phi or J-uniqueness; it packages cost and threshold hygiene those later steps rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.