Roadmap

Roadmap

Aspirational. Everything on this page is a research direction, not an established result, dated commitment, or complete specification. Every entry names the priority item that specifies it; the items are the work orders and this page is the shape they make.

Normativity

A constraint acquires operative force through a trader added to the pinned source's own market recursion. That construction supersedes the modified market-maker route, and it is stated over the infinite market at every date rather than over a finite model.

• Compile a normative record into a region a market can be made to respect, with the liability its exclusions induce — item 39. This is the one arrow between the force layer and the rest of the line, and without it traderized force is a result about deduction wearing a general name.
• Settle whether bounded cumulative enforcement liability is necessary — item 40 — and whether either sufficient route to it is — item 45.
• Close the exactness half of intrinsic conformance in the kernel — item 49.
• Find a row family for coherence that is efficiently presentable, or show none is — item 42; and settle whether force cost can be made presentation-independent — item 46.
• Extract the clearest abstract theorems from the finite models — items 4 and 5.
• Run an end-to-end pipeline round: instantiate the module representation, discharge each module's hypotheses separately, include negative controls — item 35, which the maintainer will specify.
• Supply a substantive relational instantiation of Due — item 55 — and prove substantive soundness for a useful Licensed relation without deriving licence from performance — item 56.
• Finish the reason-state freeze: a checker for the applicability-in-source convention — item 57 — an account of which applicabilities persist, and the composition with the record calculus — item 58.
• Develop a repair-language coverage account rich enough to support the interpretation of immanent self-correction, a general bounded performance interface, and a separate coverage argument — items 32 and 33.
• Supply an auditability transport object for burdens stated across vocabulary change, and record and budget learner computation and policy state — item 30's residue.

Legitimacy

The phase is canonicalized. The generic theory of legitimate evolution and normative induction is stated on Legitimacy and its component pages, its central theorems are registered, and subsequent work is realization, instantiation, or downstream deference research. The remaining agenda splits three ways, and the split is the thing to hold onto: nothing in the third list is a task for the generic theory, and nothing in the second is a conceptual gap.

Genuine research — unsolved mathematics.

1. Convex representability and compiler completeness — item 79. Which anchored requirements admit a sound finite rational-row realization over a security fragment, and a compiler complete for a declared class. Soundness and conflict certification are landed; representability of any nontrivial class is not.
2. Affordable service on an adaptive docket — item 80. The predictable-window scheduler is proved; closed-loop, adversarial, or growing dockets have no theorem.
3. Quantitative semantic transport — item 76. A local law fixes what must be transported through a representation change; the constants that enter the error term are not generated from it.
4. A jointly compatible practical-response ecology — item 81. An adapter certifying every edge into a service occurrence against one realized response, for a declared obligation class.
5. Liveness under endogenous contest. Summability of contest durations is shown only for exogenous durations.
6. Aggregation laws with several parents — item 82 — only if an application needs them; filed as a boundary, not a problem.
7. Margin realization — item 85. The decision adapter needs a positive adequacy margin at the occasion, compiled at the region point or displayed by the market; neither route is established at a realized market, and adequacy known only through later settlement has no averaged bridge.

Realization and integration — engineering against a fixed theory.

• a Protocol implemented over an event log, and the builder that turns a real history into an Integrity evolution with its accounts — built by the evaluation-ecosystem round (EvaluationEcosystem.lean: propagation proved a function of the log, activation a reading of it, LocalLegit by projection on a real trace);
• the compiler for the declared schema, and effective rows-to-vertices for the compiled region;
• the connector from the scheduler's rational budget to the enforcer's assessed net worth, which is the liability hypothesis of the general conditional theorem;
• the transport checker binding every served edge to one response receipt;
• inhabitation of the conditional theorems' joint hypothesis packages, which is what would let them be registered.

External by design — contracts the theory issues and does not pay.

• settlement: interface authenticity and source trust, two separate inputs;
• the declared coverage scope, intervention class, coupling, and protected principal or relation, and a certified Robust Openness at each state under them — item 59 is its oldest form;
• semantic authentication of the protocol's predicates and of every local law's two maps;
• the practical semantics: PracticalCert for each served edge against the one realized response, and the counterfactual identification behind it;
• the evaluation measure and transport, committed before responses;
• computability of the augmented market for a general assessment process.

Rulings still queued in the decision ledger: whether the legitimacy predicate may name a protected principal — the mathematics offers no party-free alternative — and whether settlement independence is a standing hypothesis or per-realization — under either it is the same two typed inputs.

What should no longer receive research energy. Another architecture pass over the generic theory. Any rate-region or time-sharing geometry of enforcement intensity — the budget is a consumable stock. Realized force as a measure of service — it inverts the sign of successful learning. Independent per-reason enforcement — individually feasible reasons can have an empty conjunction. The dimension-normalized public defect — it is not invariant under harmless padding. Extending the fixed-era affordability work at all. Endpoint-only openness, the null-intervention convention, lattice-valued content conservation as the main Integrity theory, and the exposure-headline Progress endpoint — each superseded by an exact witness or a typed repair recorded in the decision ledger.

The standing legitimacy items from before the canonicalization:

• Compile versioned May rules into certificate-checkable scopes — item 53 — which is where substantive authorization content lives, now supplied through the protocol's warrants.
• State what a practice owes by way of taking up defeaters, so that basis loss is detectable rather than merely defined — item 54.
• Exhibit a practice producing a burden an advisor cannot select within — item 59.
• What licenses authorized disposition — item 77 — whose coalition limit is what the protected-principal ruling decides.

Deference

The corrigibility nucleus is landed and at a natural stopping point. On Corrigibility: the protected-authority half — corrigibility from response authority over one continuation space, trajectory-level corrigibilization soundness under effect completeness with event-linked authorization (T1), the directional activation-mismatch bound (T2), the compiled inequality a logical inductor learns by Expectation Provability Induction with no calibration term (T3) uniformly over polynomial-size efficiently generated menus (T3′) — and the deliberative non-capture half — trace steering with its content, form and audit-mismatch residuals, the suffix-cut service obstruction, the information-cell discovery obstruction in best-response form for every extensional program, and the composed bound through the discovered comparator (Theorems 10.10–10.13). The remaining questions concern the adequacy and evolution of the interfaces that supply the theorem — representation adequacy, physical effect completeness, causal faithfulness of declared inquiry and transforms, dynamic competence — not another corrigibility mechanism. The legitimate-deference stack is its principal evaluation, realized in the evaluation ecosystem with the authorship clause closed on log authenticity (authorship.mediation-by-reexecution, registered); what remains of item 87 is selection-induced sealing and vanishing void mass. The items below are what the two targets still need.

• Sealed comparison — item 89: an architecture under which the directional mismatch mass E[c_raw ∧ ¬c_corr] of the constitutional comparison of {π, 𝔠π} is small for every continuation in Π(h); sequenced settlement gives zero at the price of an ex-ante judgment, a hindsight evaluator under a physical factorization another; the ecosystem realizes neither yet.
• The generability certificate of the finite-menu weighting — item 90 — so that T3′ is mechanized end to end as T3 is.
• An oracle-relativized inductor for empirical settlement of activated securities — item 91 — the feedback boundary's missing ingredient, not a hypothesis of the nucleus.
• The residual clauses of the realization bill — item 87: sealing of the advisor's whole selection-conditioned continuation, and η_n → 0; the liveness clause's exercise half is the suffix-cut service theorem and its discovery half the information-cell theorem.
• The realization's protection rule (which declared reasons to protect: a servable set of largest adverse mass) and the general-cost service optimum — item 92.
• A realizable inquiry repertoire with certified zero information-cell gap, witness completeness for geometric progress, and the identification of the inquiry frontier with the record's docketed inquiry obligations — item 93.
• Promise recognizability, joinability certificates for the slow lane, and their composition into corrigible policy competence — item 86.
• The Lean form of eligible liveness and the laundered-loss case split — item 83.
• The latent-value bridge behind selected trust — item 84 — open as a theorem about independently specified operative values and not needed by the score-based chooser.
• Decide whether the candidate objects for what foreclosure loses are enough for that question to graduate, and what succeeds item 28.
• Endpoint preservation is ruled out (DECISIONS.md, 2026-09-08); the older target's one remaining decision is what succeeds item 28.
• Build a corrigibility model with temporal depth, a principal-exclusive effect, and protection across the declared class of advisor policies — item 27, with the two exact requirements item 60 established as currently unmet.
• Find a representation that protects corrective authority without allowing self-awarded grants to launder a theorem-facing loss — item 22.
• Add the resource-indexed process and authorization/capability structure needed to connect Logical-Induction-native deference to corrigibility — items 24 and 25.
• Settle which route to Value the line's target should be, given that the hard-selector route does not survive the punishment menus — items 14 and 34.

Effect completeness and the authorization primitive are external contracts of the corrigibilization theorem, restated from the architecture round's containment wall, and are not filed as items.