Item 47: Logical Induction over an assessment process
Normativity line — traderized enforcement · difficulty substantial · project normativity · closed · node item-47
— answered by the traderized-enforcement round
Answered by the traderized-enforcement round and registered as li.assessment.* in projects/normativity/CLAIMS.md. Three strengthenings the answer carries, each because the obvious form of the theorem lacks it: nonemptiness of the world family is not a hypothesis, global nesting is not one either — only its support-local shadow — and effectiveness of the restriction lists is unused. allTrueLive_not_deductive shows the generalization is proper. Record: projects/normativity/rounds/2026-08-16-traderized-enforcement/; projects/normativity/notes/GENERALIZED_LI_PAPER_HANDOFF.md §B, Theorem 1.
Registered results bearing on this item
- li.assessment.budgeter-exploits: An exploiting trader yields a budgeted exploiting trader, over an arbitrary assessment process.
- 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-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.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
- li.assessment.firm-dominance: The generalized trading firm dominates every budgeted trader, stated against the pinned dependency's own Strategy, Trader, EF and PCWorld.
Where it hangs
- held by normativity