normativity
frame · drafted
Question
What does learning from reasons require of a reasoner: which statics a normative seed forces, how a constraint acquires operative force in a market, and what the Normative Inductor, from seed through reasons, compile, enforcement and revision, establishes end to end?
Owners: @anson (GitHub A-M-Berns) · owner has not confirmed (drafted from the wiki)
Path: the-program › normativity
Roots (the frame's goals)
plan
A seed's forced region and intervals are computed by the force layer's compiler and Fourier–Motzkin elimination, settlement nests them and defeat widens them, a form whose consequent is settled false is rebutted rather than contraposed, strict humility makes the pinned fragment seed-independent, and finitely many reasoners' intervals carry a convergence profile whose discord persists under nesting.
Logical Induction generalizes from a deductive process to an assessment process, an enforcement position compiles to a legal trading strategy with a conformance algebra, the criterion is preserved under bounded assessed liability, and for deduction the original criterion and finite-date coherence follow from a compiled market that assumes nothing about the deductive process beyond the pinned source's certificate.
For a process of normative states whose grounds are entitled in an accounted obligation state, the rowwise warrant enforcer of each date's compiled bundle on the augmented deductive market is a logical inductor, every enforced row conforms at the displayed price within the tolerance, certificate transport carries conformance to the bounds an adapter reads, and the Progress bound holds with its uptake derived.
Repeated, publicly exposed failures place diminishing weight on an inferior response under the Due, Licensed and Loss interface, through a protocol-legal, loss-blind compiler of certified surgical repairs, and the result bears the interpretation of immanent self-correction once filing and exposure connect.
An afoundational seed, one pre-licensed induction into a normative record, and a recurrent inquiry loop keep every later exercise of normative authority genealogically answerable to the practice.
shared-claim
The August 9 consolidation carries one hundred and eighty claims under its own ledger and statuses, verified continuously by the consolidation-verification gate and not re-registered.
The six open problems of the August consolidation are closed: persistence of the certified core minimum, a computable coherence modulus or a proof there is none, registry completeness for the objection grammar, higher-dimensional sharpness for the movement cap, construction of the audited pair, and schema-level demand rates.
Four extraction candidates exist for papers from the normativity line: normative serviceability and Sharp Timely Service, a liability theory for normative authority, traderization and finite-time strengthening of logical induction, and diachronic answerability under self-revision, each with its literature review completed.
What it holds
Nodes this frame is about that are not goals of the ranking: no status, value or rank here.
items (36)
- item-1: A solution to item 1 ships either a proof that a positive minimum persists under stated conditions, with necessity witnesses for those conditions; or a displayed trajectory driving it to zero under co — item 1
- item-3: A solution to item 3 ships grounds exercising every registered table, the ablation run over all thirteen, and the result either way. — item 3
- item-4: A solution to item 4 ships the multi-coordinate instances with exact witnesses, and either a sharpness proof or a witness that the predicate is not weakest. — item 4
- item-5: A solution to item 5 ships the construction, the predicates evaluated against it, and an honest statement of which clauses it does and does not inhabit. — item 5
- item-6: Item 6, Schema-level demand rates, is delivered in the shape its entry states: `enumeration-verified` over a declared finite schema family, or `conjectured` with the statement made precise. — item 6
- item-29: Item 29, Does the Φ-regret reduction instantiate on this substrate, is answered as its entry specifies. — item 29
- item-30: A solution to item 30 ships the bound or its absence, at each horizon, against the declared class; and an honest statement of whether the successful learner is still answerable and inside its declared — item 30
- item-31: Item 31, Does the objection grammar already represent a remediable-pattern filing, is delivered in the shape its entry states: `enumeration-verified` — grounds instantiating the filing against the thi — item 31
- item-32: Item 32, Extract the bounded prospective loss interface, is delivered in the shape its entry states: a typed or executable loss-generator interface exposing a bounded full-information vector on the fi — item 32
- item-33: Item 33, Separate causal transformation structure from normative certification, is delivered in the shape its entry states: a typed or executable split between compiled transformations and normative c — item 33
- item-35: Item 35, End-to-end module pipeline round, is answered as its entry specifies. — item 35
- item-40: Item 40, Is bounded cumulative enforcement liability necessary, is delivered in the shape its entry states: `witness-checked` for a refutation; `derived` or better for necessity. — item 40
- item-46: Item 46 is delivered as its entry specifies; the entry is transcribed below. — item 46
- item-41: Item 41, The safety theorem against the dependency's own construction, is answered as its entry specifies. — item 41
- item-44: Item 44, What governs removing a world from support altogether, is delivered in the shape its entry states: a stated condition, with the round's `p(A) = 0` fixture failing it and its deductive-recover — item 44
- item-45: Item 45, Is either liability bridge necessary, is delivered in the shape its entry states: `witness-checked` for a trajectory violating both bridges whose market is nonetheless inexploitable; or a pro — item 45
- item-43: Item 43 is delivered as its entry specifies; the entry is transcribed below. — item 43
- item-42: Item 42, An efficiently presentable sufficient row family for coherence, is delivered in the shape its entry states: `enumeration-verified` over a stated fragment family for a positive answer; `witnes — item 42
- item-47: Item 47, Logical Induction over an assessment process, is answered as its entry specifies. — item 47
- item-49: Item 49, A kernel proof of `DistanceComplete` for the exact dual-distance family, is delivered in the shape its entry states: `lean-proved`, discharging the `DistanceComplete` hypothesis of `exists_cr — item 49
- item-50: Item 50, The piecewise-affine facts the projection compiler cites, is answered as its entry specifies. — item 50
- item-51: Item 51, The deductive coherence region as a computable rational vertex list, is answered as its entry specifies. — item 51
- item-74: A solution to item 74 ships the theorem or the separating instance, and in either case a statement of what a certificate can and cannot be fed back into Answerability as. — item 74
- item-78: A solution to item 78 ships the rewritten pages and the registry entries; register also `LegitimateEvolution.Evolution.conservation`, `LegitimateSegment.answerable`, and `NonCapture.Scenario.robustOpe — item 78
- item-79: A solution to item 79 ships the class, the compiler, and the two theorems. — item 79
- item-80: A solution to item 80 ships the class, the theorem, and what it does to the residual term. — item 80
- item-81: A solution to item 81 ships the adapter, its theorem, and the class it covers. — item 81
- item-82: A solution to item 82 ships the extension, or a statement that no application needs it. — item 82
- item-85: A solution to item 85 ships the composed theorems, or the negatives. — item 85
- item-112: Item 112, Occurrence-level defeat: the orphan pin, is delivered in the shape its entry states: the rule as a `def` on `Grounds` replacing `Grounds.region`'s port-only filter, the no-orphan theorem on — item 112
- item-113: Item 113, Settlement defeat for strength rows: a linear row contraposes, is delivered in the shape its entry states: the chosen condition as a `Form`-level rule, the monotonicity statement it keeps or — item 113
- item-114: Item 114, The pinned-region divergence against the pinned market maker, is delivered in the shape its entry states: `derived` or better: a Lean statement over `history L E` with the trader exhibited, — item 114
- item-116: Item 116, The record as reason trace: what it mediates, the defect, and the port's duplicate, is delivered in the shape its entry states: (a) and (b) as filed positions with fixtures; (c) a deletion. — item 116
- item-125: Item 125, Distance-to-region conformance for the rowwise enforcer, is delivered in the shape its entry states: `lean-proved` either way; if the Hoffman route, the constant as a `def` on `Bundle` with — item 125
- item-126: Item 126, The bankroll across repeated reopenings, is delivered in the shape its entry states: `lean-proved` on `OddsBankroll.Account`. — item 126
- item-127: Item 127, Defeaters as undercutting occurrences: the grounded extension with attacks, is delivered in the shape its entry states: `lean-proved`; the agreement theorem. — item 127
Sub-frames
- seed-theory: What does a normative seed force on the prices of a settled fragment, how does that change under settlement, defeat and rebuttal, and do reasoners starting from different seeds end up anywhere together?
- operative-force: How does a constraint acquire operative force in a logical inductor's market without destroying the property that nobody can pump the reasoner, and what does that force cost?
- normative-inductor: Does a logical inductor made to answer to legitimately incurred obligations, through an enforcer on the compiled region of the entitled record, remain a logical inductor and deliver the Progress bound, and what remains conditional in that theorem?
- response-learning: Does a bounded learner, given due burdens, licensed responses and a bounded prospective loss, reduce a recurrent publicly represented failure by lawful edits, and with which coverage does that bear the interpretation of a lesson?
- normative-record: Before a learner can answer a demand, what determines why the demand arose, how evidence enters the practice, what authorizes a normative response, and what keeps an unanswered question from vanishing?
Narrative: Normativity
Normativity
Normativity asks what it means for a changing reasoner to remain responsive to reasons. A fixed objective can score behavior from outside. This project instead asks how warrants, challenges, permissions, and failures can be represented in a public practice that the reasoner participates in without giving the reasoner unilateral control over the score.
The line moves from static assessment to learning:
- A relational score records what one participant attributes to another.
- A quantitative book projects parts of that score into exact constraints and accounted quantities.
- Answerability determines when a participant owes an answer.
- A response-learning theorem asks whether repeated, publicly exposed failures place diminishing weight on an inferior response.
Reasons, Answerability, and the Score develops the first three layers. Normative Response Learning explains the current Due / Licensed / Performance interface and conditional theorem.
Core idea
A practice can assess a response without pretending to possess a view from nowhere. Participant i may attribute commitments and entitlements to participant j using i's inferential practice and j's public acknowledgments. A challenge then has a source, a target, and a standing relation. Disagreement is represented rather than averaged away.
The quantitative layer is downstream of that representation. It uses bounds, holdings, intervals, charges, and caps to make finite questions exact. Leverage survives only as the name of a technical quantity: how far a forced interval endpoint clears a relevant threshold.
Learning adds a further demand. Static admissibility can say that a response is allowed now. It does not show that a bounded learner will stop repeating a recognized failure. That requires an explicit response space, a loss-blind compiler of lawful edits, a performance margin, learning dynamics, and enough coverage for the relevant burdens to recur.
Current status
**Established —
lean-proved.** The traderization arc is the line's registered result: Logical Induction generalized from a deductive process to an assessment process, the enforcement position as a legal strategy with its conformance algebra, preservation of the criterion under bounded assessed liability, and — for deduction — the original criterion together with finite-date coherence, from a compiled market that assumes nothing about the deductive process beyond the pinned source's own certificate. The 64 entries in this line's registry each name a Lean declaration and the priority item it answers.
Open / unregistered research. The frozen consolidation is a separate 180-claim foundation with its own ledger and status vocabulary. The modern workspace registry does not translate or promote those claims. The current response-learning theorem and dynamics witness remain unregistered.
The abstract response-learning theorem is settled at its stated conditional interface level. The normative content remains open: there is no satisfactory substantive Due, no proof of substantive soundness for Licensed, no general performance theory, and no delivered coverage conclusion. An audit transport object for liabilities stated across vocabulary change is also absent. What the registered results establish is force, not legitimacy: the map from a normative record to a region a market can be made to respect is specified by the Normative Inductor's compiler contract and not yet proved.
The seed, and rebuttal by settlement
The left input of the compiler now has a page of its own: Seed Theory. A seed's forced region and intervals are computed on the force layer's own compiler, settlement nests them and defeat widens them, and since the rebuttal round a form whose consequent is settled false is rebutted rather than contraposed — the repair to the orphan pin the warrant round <a class="ref round" href="/rounds/2026-10-20-warrant-enforcement-semantics/">[round]</a> exhibited. The first end-to-end run of the pipeline on one fixture is the witness <a class="ref round" href="/rounds/2026-10-21-rebuttal-and-end-to-end/">[round]</a>.
A current research direction: operative force
A constraint that cannot change what a reasoner does is a description of the reasoner, not a demand on it. So a normative architecture needs an account of how a constraint acquires operative force — and that account should not be supplied by fiat, as an unexplained primitive of whatever dynamics the reasoner runs.
One candidate is to make the constraint a participant. If the reasoner's credal state is a set of prices in a market, an admissible region can be given force by a distinguished trader that trades against violations of it: when the displayed price leaves the region, the trader takes a position whose payoff improves as the price moves back in, and the market's own price-setting has to answer it.
Two distinctions the work turns on.
Constraint source versus enforcement mechanism. The mechanism is indifferent to where the region comes from. Logical consequence, a settled record, a trusted process and an endorsed normative book are all sources, and one enforcement mechanism can serve any of them — provided the source delivers something the mechanism can consume, which is not a set but a finite system of rational inequalities. A source that names a region without presenting it that way names nothing the mechanism can act on.
Force versus legitimacy. Force turns out to be cheap. Any nonempty region with a presentation gets it, at any trading intensity, and the mechanism will hold a region that fixes a single credal state exactly as readily as a defensible one. Whoever writes the inequalities therefore sets the reasoner's beliefs, which makes this a channel for manipulation before it is anything else. Operative force is no evidence of legitimacy, and this direction supplies no legitimacy result. It sharpens the question by separating it cleanly from a mechanism it might otherwise be confused with.
Deduction as the calibration case
Ordinary deduction fits. What a deductive process has settled by a given date determines the credal states some distribution over the still-possible worlds reproduces, and enforcing membership in that region is a finite-date version of a coherence property logical inductors otherwise obtain only in the limit.
It is also the free case. The enforcing participant's position is worth nothing lost in any world the region contains, so where the region admits every world deduction has not ruled out, it never shows a loss a live world would recognise and the market's resistance to being pumped survives untouched. Deduction has that property by construction, which makes it the instrument the other sources are read against rather than one instance among equals.
What a normative constraint does differently is exclude states deduction permits — that is what it is for — and excluding a world that is still live is what makes the enforcing participant lose. But the cost is not a wall. It is a quantity, depending on how much ordinary trading pressure there is, how deep the exclusion cuts, and how tightly the mechanism has promised to enforce. A source may exclude live worlds permanently and still be safe, provided that quantity stays summable over time. Not agreement with deduction, then; convergence on it, at a rate.
What a constraint is, and what a market can see of it
Underneath this sits a distinction that took the work several attempts to state correctly, and getting it right turned out to improve the picture rather than merely repair it.
A constraint of this kind is really a restriction on distributions over possible worlds, not on any single world and not on prices. Which worlds still count as possible is then read off by asking which ones some permitted distribution takes seriously — gives positive weight to. A constraint saying "no more than even odds on A" does not make A impossible; it permits the even-odds distribution, which takes A perfectly seriously.
What a market sees is much less than that. Prices record only the averages a distribution induces on the sentences being priced. And averages do not determine the distribution: two quite different restrictions can produce exactly the same prices while disagreeing about which worlds are possible at all. The smallest example needs two sentences and says that deduction has established they agree — prices then pin p(A) = p(B), and the distribution that is certain they disagree, half one way and half the other, produces exactly those prices while being ruled out entirely.
So prices are enough to push a reasoner around and not enough to say what it believes. That is the reason this direction has two channels rather than one, and it is a fact about information rather than an awkwardness of mechanism. The enforcement mechanism works on the prices; what the reasoner is answerable to is the constraint the prices only partly reveal.
It also sharpens what remains open. The mechanism's guarantee is about averages; being resistant to a pump is about individual worlds. Bridging the two takes a further assumption — about how far the constraint's demands sit from the world in question, or about how much weight that world can carry — and which assumption is right is not settled.
What a norm has to promise in exchange for force
The question that decides whether any of this is usable is not whether prices can be pushed exactly onto a demand. It is whether pushing them destroys the property that made the reasoner worth having: that nobody can pump it indefinitely.
Splitting the demand helps. The part that merely records what has been settled costs nothing to enforce — no still-possible world disagrees with it, so the participant enforcing it never loses to anyone. The part where a norm genuinely outruns the record is where the cost lives, and the cost is governed by one quantity: how far the norm's demand exceeds what the least favourable still-possible world delivers. Notably it does not depend on how hard the norm is enforced.
Settlement pushes that quantity down and never back up, which helps and is not enough on its own. What is missing is an account: the practice has to be willing to say in advance how much its norms are allowed to cost while they run ahead of what has been established, and to stop when that is spent. The line's existing work already imposes exactly that discipline on a different object, for the same reason — a claim can survive any number of tests if someone keeps quietly paying for its losses.
So the shape is: one clause says what force a norm gets, and another says how much damage granting it may do.
Force, and what force costs
Two things about this mechanism are worth separating from the idea that motivated it.
It leaves the reasoner's own price-setting alone. That matters more than it sounds: the alternative way to make a region operative is to constrain the price-setting directly, and a price-setter required to respect a region can be handed demands it cannot jointly meet. Adding a participant instead changes only what the existing machinery is responding to, and everything already known about that machinery keeps applying.
And there is a trade the mechanism cannot presently escape. A participant whose position shrinks as the violation does is safe — it never loses where the region is right — but it can be neutralised by ordinary traders near the boundary, so what it delivers is conformance to a declared tolerance rather than exact membership. A participant that holds a floor outside the region can deliver exact membership, and pays for it by holding positions where nothing is wrong, which is where its losses come from. Whether one participant can do both is open.
Where exactness is available turns on geometry, and not in the way one might guess. A constraint that pins a sentence to certainty — the shape a settled fact takes — is the easy case: it sits on a face of the space of possible prices, and a participant pushing outward from that face costs nothing to leave in place. The hard case is a constraint sitting strictly inside, of the kind a relation between sentences produces, where the participant must change direction as the price crosses it and continuity leaves a band it cannot hold. The general characterisation is not settled, and tolerance is what the surrounding machinery was built to consume anyway.
Where it sits
This is a layer beneath the statics rather than a rival to them, and it is one layer among several. Which sources may define admissible regions is a question of constitution and legitimacy; whether a requested region is coherent and non-empty is feasibility; who may write, revise, object or be held to account is answerability; and how an agent improves among the responses it is permitted is learning. Force is only the question of how a region, once validated, reaches behaviour at all — and keeping the five apart is most of what this direction has so far established.
The response-learning interface governs how an agent learns among responses; force governs which credal states it may display. The arrow between a normative record and a region in price space is the proof-carrying compiler of the Normative Inductor: it takes legitimately incurred obligations to one joint convex region per service date, and the force mechanism here enforces that region. The compiler's soundness and completeness are stated as realization obligations, not proved, so the general reading is a specified interface with deduction as its only kernel-checked instance. For Deference the direction is downstream, not a solution — a trusted process's constraint can be made operative this way while authorization, corrective control and futurity remain exactly as open as before.
Force also turns out to be bought rather than granted. Giving a constraint operative force means running an externally funded trader against violations, and an externally funded trader is exactly what Logical Induction's no-exploitation guarantee is not built to survive. What rescues it is a finite cumulative account: each date's force costs (slack + ordinary volume) × exclusion depth ÷ tolerance, charged before the trade is emitted, and the remaining account is what determines how tightly the reasoner may be forced. Two things the account is not is worth saying, because both look sufficient and neither is: capping each endorsement separately fails, since finitely many caps need not sum, and capping how many constraints are live per date fails, since nothing bounds the number of dates.
What a date of force costs is a product of three quantities — how much ordinary market pressure it must push against, how far its demand outruns what the record supports, and how much error it tolerates — and the account holds whenever that product is summable. None of the three has to shrink on its own. A demand can stay exactly as far from the record as it ever was, forever, and remain affordable if the market pressure it faces decays; only when pressure and distance are both pinned and the tolerance is capped does the account necessarily run out.
An earlier reading of this said the normative distance itself had to close. It does not, and the difference matters for what the picture claims: safety does not require that disagreement be settled, nor that it narrow — only that resisting it get cheaper by some route.
The motivating statics do produce a demand that is never vindicated and stays affordable indefinitely, though not from every kind of demand: a constraint on a single sentence holds its distance and then closes it in one step, while a graded demand sitting at the value the record approaches can be enforced forever.
Evidence: the traderized-enforcement round <a class="ref round" href="/rounds/2026-08-16-traderized-enforcement/">[round]</a>.
Evidence and deeper reading
Statement
A reasoner that answers to legitimately incurred obligations without ceasing to be a logical inductor exists as a conditional theorem, built from the seed statics, operative force bought under a finite liability account, a proof-carrying compiler from the accounted record to a region, and the response-learning bound.
Source
wiki/Normativity.md, Core idea and Current status (the traderization arc registered; force, not legitimacy, established); wiki/Normative-Inductor.md, The architecture and The conditional theorems; wiki/Seed-Theory.md; wiki/Roadmap.md, Normativity; projects/normativity/CLAIMS.md.
Notes
The normativity line (ruling M2). Its roots: the programmes this round drafted from the wiki per ruling M3 (seed-theory, operative-force, normative-inductor, response-learning and the unspelled normative-record) and, since the follow-up of 2026-10-23 dissolved the pre-existing frame normativity-line (ruling F4), the line-level claims that frame held and no programme asks for: the August 9 foundation, the six consolidation problems and the paper candidates; its fixed-era layer sits under normative-inductor, its traderization step under operative-force and its learning track under response-learning. The line holds (holds, ruling G2 of 2026-10-23: attached, listed, no goal of the ranking) every item of project normativity no finer goal was identified for; until that ruling they hung in docket-normativity, an or root, now deleted. Drafted by prompts/2026-10-22-map-as-canonical; the owner has not confirmed the decomposition.
Author and human events
Author @smithy-verity; version 1; size L.
No human event has touched this node.
Edges
Above
- part of the-program
- root (plan) of the-program
Children
- part: seed-theory frame
- part: operative-force frame
- part: normative-inductor frame
- part: response-learning frame
- part: normative-record frame
- part: normativity-aug9-foundation leaf/step
- part: normativity-consolidation-open-1-6 leaf/question
- part: normativity-paper-candidates leaf/step
Work pointers
- decision the map is the canonical index of the program: two maintainer handles, one plan with seven lines, programmes drafted from the wiki, the map as the foundational layer, multi-owner frames, `PRIORITIES.md` as a render, decision anchors, and the structure-only index (M1–M8)
- decision the map's follow-up rulings: hypotheses are filed when read, the registry join is an edge, the large derived files leave the tree, one decomposition per line, a formal result sits under the claim it establishes, and items are docketed by programme (F1–F6)
- round 2026-08-11-phi-regret-applicability
- round 2026-08-11-phi-regret-bridge
- round 2026-08-11-phi-regret-learner
- round 2026-08-11-phi-regret-prep
- round 2026-08-13-crown-jewel-learning-theorem
- round 2026-08-13-crown-jewel-learning-theorem-final
- round 2026-08-13-crown-jewel-learning-theorem-refinement
- round 2026-08-13-local-regret-normative-learning
- round 2026-08-13-wikification-and-normativity
Ranking (the lens, not the structure)
{
"status": "open",
"diagnosis": null,
"flags": [
"owner has not confirmed (drafted from wiki/Normativity.md)"
],
"V": {
"V_prior": null,
"display": "2",
"headline": 2,
"ref": 2,
"valid": 2,
"weaker": "both"
},
"belief": null,
"draft": "ai",
"root": {
"status": "open",
"Pr": {
"hi": "0/1",
"lo": "0/1",
"mid": "0/1"
},
"value": null,
"cost": "85/1",
"margin": "no established leaves"
}
}Say something about it
Each verb opens a prefilled issue; a round files what lands as the ledger event it is.