ForcingChainComp3Cert
plain-language theorem explainer
Certificate bundle of three analytic facts on the domain cost used in the T0–T8 completeness module: the cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. Pure structure definition; no proof body.
Claim. A forcing-chain completeness certificate is a triple of properties: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all $m,e > 0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module packages the T0–T8 forcing chain as a structural completeness theorem derived from the J-cost: uniqueness of $J$, the Recognition Composition Law, Noether charges, the golden ratio fixed point $\varphi$, the eight-tick period, $D=3$, $\alpha$, and $\Lambda$, with zero sorry and zero axioms.
The domain cost is the real-valued cost assigned to a pair of positive scales (measure and event). Upstream, recognition-event cost is already known to be nonnegative via $J$-cost nonnegativity on positive states. The canonical threshold is the positive cutoff used to separate trivial from nontrivial recognition in the completeness argument.
The structure does not prove those facts; it names the three Prop fields a later inhabitant must supply.
proof idea
No proof: this is a structure declaration. The three fields are Prop-valued requirements (cost_at_eq, cost_nonneg, threshold_pos). The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge them when the concrete cert value is built.
why it matters
Gives a single named type for the analytic side-conditions of Forcing Chain Completeness (Plan v7). Downstream, cert fills the three fields from the sibling lemmas, and cert_inhabited records Nonempty ForcingChainComp3Cert. That inhabitation is the module's structural claim that the cost/threshold package needed for the T0–T8 derivation is available inside Lean, tying the J-cost nonnegativity line (ObserverForcing) into the completeness certificate without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.