StrengthClaim
plain-language theorem explainer
An audit record pairing a named PRC claim with a commitment-strength tag and a human-readable statement string. Downstream premise ledgers and boundary certificates cite it to itemize what each deposit assumes. As a plain structure with three fields and Repr, there is no proof content.
Claim. A strength claim is a triple $(\ell, \tau, s)$ where $\ell$ is a label string, $\tau$ is a strength tag (one of: $\delta$-only, trace closure, choice, power comprehension, classical extension), and $s$ is a statement string describing the mathematical content being audited.
background
In the Primitive Recognition Calculus, every deposited claim is tagged by how much it assumes beyond bare distinction. The strength tag inductive type ranks five levels: $\delta$-only (forced by distinction and finite repetition alone), trace closure (completed orbits or stable trace families), choice (witness selection from stable families), power comprehension (controlled subtrace or power-class formation), and classical extension (excluded middle or full classical reasoning).
Commitment rank turns those tags into an ordered ledger: $\delta$-only has rank 0, each later tag strictly higher, up to classical extension at rank 4. The order is the numerical comparison of ranks, and injectivity of rank makes the order antisymmetric rather than a collapsed preorder. This mirrors the pretemporal forcing-order ranks and the objecthood-registry commitments (forced, permitted, quotient, completion, display), but is specialized to PRC claim strength.
The local module packages the tag, its rank, the $\le$/$\lt$ instances, and the strict chain $\delta$-only $<$ trace closure $<$ choice $<$ power comprehension $<$ classical extension as the K1 Strength Ledger anchor.
proof idea
Definitional structure only: three fields (label, tag, statement) with a derived Repr instance. No tactics, no lemmas, no proof obligations. Downstream sites construct concrete values by supplying a string label, a StrengthTag constructor, and a statement string.
why it matters
This is the carrier type for the K1 Strength Ledger. Every audited PRC deposit builds a list of these records so a referee can see, tag by tag, what was assumed. Downstream uses include the native cost-selection premise ledgers (base reciprocity and RCL hypotheses tagged $\delta$-only), the real-Cauchy and real-null-setoid claims (tagged trace closure), the trace-closure boundary certificate K4.13, and the real-completion boundary K4.14 (tagged classical extension until an internal PRC Cauchy quotient exists).
The structure makes the honesty claim type-checkable: moving from the $\delta$-native carrier to continuous completion is a real strengthening (rank 0 to rank 1), not a free step. That separation feeds the broader forcing narrative (distinction first, completion later) without smuggling classical analysis into the primitive layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.