operative-force
frame · drafted
Question
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?
Owners: @anson (GitHub A-M-Berns) · owner has not confirmed (drafted from the wiki)
Path: the-program › normativity › operative-force
Roots (the frame's goals)
shared-claim
A constraint on prices compiles to a legal trading strategy in the market recursion, the modified market is a logical inductor over an assessment process, and the deductive coherence region is a computable rational vertex list.
A constraint on prices compiles to a legal trading strategy inside the market recursion, giving per-date conformance within a schedule while preserving the logical induction criterion.
The compiled per-date conformance, in which a constraint on prices compiles to a legal trading strategy that conforms within a schedule while preserving the criterion, can be improved until it reflects a logical inductor whose prices answer a normative seed's constraints under a finite liability account well.
What it holds
Nodes this frame is about that are not goals of the ranking: no status, value or rank here.
formal results (26)
- li.assessment.budgeter-value: The registered claim li.assessment.budgeter-value (lem:budgeter 1 over an assessment process) holds as its declaration states it; the registry's note is quoted in the Source.
- li.assessment.budgeter-floor: The budgeted trader's net worth has the source's floor at every plausible assessment. Nonemptiness of the world family is not a hypothesis: the scaling infimum over an empty plausible set is one.
- li.assessment.budgeter-exploits: An exploiting trader yields a budgeted exploiting trader, over an arbitrary assessment process.
- li.assessment.firm-dominance: The generalized trading firm dominates every budgeted trader, stated against the pinned dependency's own Strategy, Trader, EF and PCWorld.
- li.assessment.criterion: MarketMaker applied to the generalized trading firm satisfies the exploitation criterion relative to the assessment process. The market-computability premise is carried exactly as the pinned source ca
- force.strategy-value: The compiled enforcement position is a legal Strategy whose value against a payout table is exactly the quantity the force inequalities bound. Without this identity those inequalities are algebra abou
- force.row-tolerance: Positivity of the disturbance is load-bearing and is carried in the statement: at zero disturbance the intensity condition is met by a zero intensity, which enforces nothing.
- force.preservation: Sufficiency only. The converse is item 40 and the forward proof discards information, so this is not an equivalence.
- force.deductive-day-nonneg: Every deductively plausible world lies in the coherence polytope, so the enforcement position's day value is nonnegative there for any nonnegative intensity.
- force.deductive-cumulative-nonneg: Per-date nonnegativity summed. This is why deduction is the free case rather than one instance among equals: the risk capital is exactly zero, so no affordability side-condition binds and the toleranc
- force.deductive-criterion: The dominance step is the pinned source's own trading_firm_dominance at its own DeductiveProcess, so the conclusion is the source's criterion over D rather than a generalization of it.
- force.deductive-inductor: The criterion form, assembled as the dependency's own IsLogicalInductor. Its computable-market hypothesis is discharged separately by the projection arc's compiler.
- force.deductive-witness: A deductive process revealing one atom, an added trader, and the liability bound derived from the force algebra rather than assumed, at a presentation a legal price can violate. A theorem whose hypoth
- coherence.modulus-soundness: The soundness half of the coherence measure. It does not answer item 42, which asks for a polynomially presentable family; it is the half of the measure item 42's narrowing is stated against.
- coherence.modulus-net-cover: Conformance at tolerance on an l1-net of a stated mesh bounds every support gap by tolerance plus mesh, with Lipschitz constant one. The constant is attained, so the bound is sharp; row conformance on
- compiler.schedule-end-to-end: No supplied market, region or representation. The one standing hypothesis is that the enforcer's trade map is primitive recursive, which is the definition of an effective enforcer and sits where the s
- compiler.constraints-end-to-end: The generic form over a rational constraint schedule, written a second time over raw non-dependent data because the structured pipeline's types are not Primcodable. The obstruction was never that the
- maxmin.representation: Ovchinnikov Theorem 4.1(a), for a nonempty convex domain in a topological real vector space. The source's proof silently needs full-dimensionality; the statement does not, and the round's errata carry
- maxmin.converse: Theorem 4.1(b). The agreement obligation quantifies over all pieces, including index triples outside the relevant selection sets, so each piece carries a guard.
- region.patterns-sound: Stated with the rational payout table rather than the real-valued one, which is what makes the list rational; the two agree by the repository's existing payout identity.
- region.patterns-complete: Completeness over the priced fragment, with no hypothesis on the fragment: coordinates may repeat or be empty.
- region.patterns-nonempty-iff: A biconditional, so the satisfiability hypothesis is exact rather than merely sufficient: no weaker hypothesis suffices and no stronger one is used.
- region.hull: An image equality, which is the form with content: membership is defined through the hull, so the unfolding form is definitional and says nothing. Duplicate-freeness of the fragment is used in the sur
- smoke.faf-asymp-refl: Reaches a real declaration in the pinned dependency. Certifies the chain, not mathematics.
- smoke.chain-compiles: States a Mathlib limit in the dependency's own vocabulary, so it typechecks only if both halves of the chain agree.
- simplex.rational-points-sum-to-one: A worked example of the schema, not a research result: the house enumeration checker generates the 28 rational simplex points at denominator six and confirms each sums to one. It exists so the registr
items (1)
Narrative: Actionability-and-Normative-Force
Actionability and normative force
Status: the enforcement construction's three narrow results are **Established — lean-proved**. The action theory built on them is open / unregistered and is realization material: its force, intensity and uptake distinctions enter the canonical theory only as the uptake certificate of normative induction.
What it means for a reason to have force
A reason that changes nothing is not exerting normative pressure; it is being recorded. So the program needs an account of how a constraint on what a reasoner ought to believe becomes something that actually moves what it does believe — without that account being either "we hard-code the constraint" or "we hope the reasoner cooperates".
The construction is this. The reasoner's beliefs are prices in a market. A constraint becomes a trader: a position that buys against the constraint's violation, added to the aggregate the market maker prices against. It is an ordinary participant, playing by the ordinary rules. Because the market maker itself is untouched, every guarantee about the market maker survives intact.
What you get is a per-moment conformance bound: at any price the market maker will accept, the constraint is violated by no more than a declared tolerance. Turn up the intensity and the tolerance tightens.
Notice the shape of that. The underlying construction guarantees only that exploitation vanishes eventually; this gives a bound at a date. That is a finite-time strengthening of a well-known asymptotic guarantee, and it engages a standing criticism of the original — that asymptotic inexploitability leaves finite behaviour almost unconstrained.
The thing force does not give you
Force is not a semantics: it operates on a region in price space, and whether that region correctly expresses a normative demand is a separate lift.
Force is not a legitimacy certificate: nothing about compiling a constraint says the constraint should have been there.
Force is not free. What it emits alongside the conformance guarantee is a liability obligation that some other layer has to discharge.
Actionability: what a unit of enforcement accomplishes
Given that pressure can be applied, how much correction does applying it buy?
The general form is: some amount of intensity, spent against some defect, yields work; and if the work per unit of intensity tends to zero while the total intensity diverges, the defect must be vanishing. The precise condition is exactly what you would want it to be and nothing more:
Correction converges if and only if the work a defect generates is bounded away from zero whenever the defect is bounded away from zero.
Convexity is not needed. It buys the rate, and only that. The projection enforcement used in the concrete construction has a quadratic modulus and gets the square-root rate; an older linear form gets a different one. One theorem covers both, and the rate reads off the modulus.
This is a small result with a useful moral: several earlier statements in the program carried convexity as a hypothesis, and it turned out to be doing no work at the level of convergence.
Several reasons at once
Does a certificate that enforcement helps reason A, and a certificate that it helps reason B, give one that it helps both?
Not if each reason is scored against its own region. There is an exhibited pair whose demands are jointly satisfiable and whose per-reason gain after aggregation is negative — each reason's correction, evaluated in that reason's own terms, is made worse by the other's.
Yes if both are scored against the region they share, with no convexity and no separability assumption.
In the concrete construction this turns out to be true and unused: the compiled position responds to the actual prices rather than being assembled from per-reason commitments, so there is no aggregation step at which a per-reason certificate could be invalidated. The failure mode is real for a different architecture, and knowing which architecture has it is the point. The Normative Inductor takes the same side: every constraint serviced at a date is compiled into one joint convex region, and two individually feasible constraints with an empty conjunction are reported as a conflict that conserves both, never run as two enforcers against each other.
What gets scheduled, and what merely happens
One typing decision, because getting it wrong inverts the sign of everything downstream.
The natural reading of "how much did we serve this reason" is how hard did the enforcement position push. That reading is wrong three times over. The push is decided at the market's fixed point, so no scheduler can choose it. It is zero exactly when the reason is perfectly satisfied, so the measure is undefined in the best case. And it counts a moment as better served precisely because the reasoner behaved worse.
Three things need keeping apart, and only the middle one is chosen:
- service — the broad relation this program cares about: an obligation receives the answering work it is owed. This is Answerability-facing and says nothing about markets;
- enforcement intensity — the scalar a scheduler fixes in advance, before any price is set. In this realization it is the resource by which service is supplied, and it is predictable and freely schedulable, which is what makes scheduling a well-posed question at all;
- realized force — the corrective position that actually materializes at the fixed point. Endogenous, and not anybody's to choose.
Service is not identical to enforcement intensity. Intensity is how a market-embedded reasoner happens to pay for service; a different realization could pay for it some other way.
Under the wrong reading, successful learning looks like starvation: a reasoner whose defect decays geometrically under constant intensity has total realized force that converges, and appears to be receiving less and less service the better it does.
Where this sits
Actionability is not downstream of scheduling and it is not upstream of it — it sits beside it. Answerability fixes what is owed; Actionability fixes what a unit of enforcement accomplishes; the scheduler fixes how much intensity goes where. Progress needs all three and derives none of them from the others.
Evidence. The kernel-checked results are in [2026-08-16-traderized-enforcement](https://github.com/A-M-Berns/alignment-workspace/tree/939c459974fd1a7365f2c050e883eb1a630123cc/projects/normativity/rounds/2026-08-16-traderized-enforcement) <a class="ref round" href="/rounds/2026-08-16-traderized-enforcement/">[round]</a>, with the caller-facing summary in [TRADERIZED_FORCE_INTERFACE.md](https://github.com/A-M-Berns/alignment-workspace/blob/939c459974fd1a7365f2c050e883eb1a630123cc/projects/normativity/notes/TRADERIZED_FORCE_INTERFACE.md). The action theory is [FIXED_ERA_THEOREM.md](https://github.com/A-M-Berns/alignment-workspace/blob/939c459974fd1a7365f2c050e883eb1a630123cc/projects/normativity/legitimacy/rounds/2026-08-31-normative-affordability/FIXED_ERA_THEOREM.md) <a class="ref round" href="/rounds/2026-08-31-normative-affordability/">[round]</a> §1 and the typing argument is [SERVICE_FORCE_TYPING.md](https://github.com/A-M-Berns/alignment-workspace/blob/939c459974fd1a7365f2c050e883eb1a630123cc/projects/normativity/legitimacy/rounds/2026-08-31-normative-affordability/SERVICE_FORCE_TYPING.md) <a class="ref round" href="/rounds/2026-08-31-normative-affordability/">[round]</a>.
Statement
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.
Source
wiki/Normativity.md, A current research direction: operative force, and Current status; wiki/Actionability-and-Normative-Force.md; projects/normativity/CLAIMS.md, The traderization arc; projects/normativity/notes/GENERALIZED_LI_PAPER_HANDOFF.md.
Notes
Drafted from the wiki per ruling M3 (prompts/2026-10-22-map-as-canonical); the owner has not confirmed. The traderization step filed before this round (traderization-arc, a root of this frame since the follow-up of 2026-10-23 dissolved normativity-line) names the same arc as an actioned claim; this frame holds the arc's registered results as formal results (holds, ruling G2 of 2026-10-23: held, not roots) and item 39; the other work orders of the section Normativity line — traderized enforcement are held by the normativity line.
Author and human events
Author @smithy-verity; version 1; size L.
No human event has touched this node.
Edges
Above
- part of normativity
- root (plan) of normativity
Children
- part: traderization-arc leaf/step
- part: traderized-finite-date-conformance and
- part: traderized-finite-date-conformance.improvable or
Ranking (the lens, not the structure)
{
"status": "open",
"diagnosis": null,
"flags": [
"owner has not confirmed (drafted from wiki/Actionability-and-Normative-Force.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": "240/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.