inductor.contraposition-blocked
and · drafted
Statement
At date 9 of Scenario B the specialized strength row reads 2/3·P(X∧A) ≤ 0 while the enforced applicability row with X settled true forces P(X∧A) ≥ 3/4 (antecedent_open): the date-9 bundle with the strength row appended has empty region. Rebuttal by settlement removes the row, so the antecedent's credence stays where the applicability puts it rather than being suppressed by contraposition.
Source
projects/normativity/CLAIMS.md, entry inductor.contraposition-blocked (class lean-proved, status active, origin round 2026-10-23-normative-inductor-consolidation; answers item 113). Documentation: verification: projects/normativity/rounds/2026-10-23-normative-inductor-consolidation/THEOREM.md; context: projects/normativity/rounds/2026-10-23-normative-inductor-consolidation/THEOREM_STORY.md. The signature of Workspace.Normativity.Contrib.WarrantInductorRebuttal.contraposition_blocked in lean/Workspace/Normativity/Contrib/WarrantInductorRebuttal.lean.
Notes
Filed by the map-as-canonical round (prompts/2026-10-22-map-as-canonical) from the registry entry and the declaration's signature; its hypotheses are unread (ruling F1, 2026-10-23): the record's Source carries the signature verbatim, and a reader files the hypothesis leaves. Registry note: At date 9 of Scenario B the specialized strength row reads 2/3·P(X∧A) ≤ 0 while the enforced applicability row with X settled true forces P(X∧A) ≥ 3/4 (antecedent_open): the date-9 bundle with the strength row appended has empty region. Rebuttal by settlement removes the row, so the antecedent's credence stays where the applicability puts it rather than being suppressed by contraposition. The registry's answers_item is the priorities pointer to item 113 (ruling F2).
Bridge card
Connected to no informal claim yet: held by normative-inductor.
Declaration Workspace.Normativity.Contrib.WarrantInductorRebuttal.contraposition_blocked in lean/Workspace/Normativity/Contrib/WarrantInductorRebuttal.lean (record inductor.contraposition-blocked.record)
Registry inductor.contraposition-blocked: class lean-proved, status active, review ci-only, origin round 2026-10-23-normative-inductor-consolidation; bears on item 113
The statement of record of `inductor.contraposition-blocked` formalizes the registered claim as the registry reads it: rebuttal withdraws the strength row that, kept, would have made the compiled system infeasible.
Hypotheses: unread (the record's Source carries the signature; a reader files them).
Completeness (inductor.contraposition-blocked.complete): No premise beyond the signature's binders enters the declaration; the kernel checks it as stated. The result is the record, this leaf and the bridge, and its hypotheses are unread: the record's Source carries the signature verbatim and no hypothesis leaf is filed until a reader files one.
Author and human events
Author @smithy-verity; version 1; size M.
No human event has touched this node.
Edges
Above
- held by normative-inductor
Children
- part: inductor.contraposition-blocked.record leaf/record
- part: inductor.contraposition-blocked.bridge leaf/bridge
- part: inductor.contraposition-blocked.complete leaf/completeness
Work pointers
Ranking (the lens, not the structure)
{
"status": "open",
"diagnosis": null,
"flags": [
"held by normative-inductor",
"hypotheses unread"
],
"V": {
"V_prior": null,
"display": "2",
"headline": 2,
"ref": 2,
"valid": 2,
"weaker": "both"
},
"belief": null,
"draft": "ai"
}Say something about it
Each verb opens a prefilled issue; a round files what lands as the ledger event it is.