updateless-dt-programme

UDT is specified over a logical-induction belief process by treating the process's future belief states as observations, with a Bayesian logical inductor supplying coherent probabilities over the large sentences that describe those states, and the resulting agent satisfies a tiling theorem, by at least one of four routes: the trajectory prior B1, the measure-valued B3, a linked B2, or BLI's constraints derived from real-value coherence.

An agent acquires UDT-like behaviour by learning, with policy-level optimality built into the loss principle that guides learning, by at least one of: an LI/BRIA agent meeting the acceptance statement together with its updateless extension on a declared recovery domain; policy selection over logical induction with a theorem behind it.

The counterfactuals an embedded agent's decision rule uses are specified in both halves: for decision problems with predictors, the referent the formal core's counterfactual structure is calibrated to; for logical counterfactuals, Troll Bridge and its Löbian lesion classified in provability logic with their logical-induction forms decided.

The decision-problems formal core, trees over decision points with subjective states in Jeffrey–Bolker–Joyce format, calibration, consistency and coherence, reaches the next revision of Coherent Care, in which the UDT-versus-EDT compatibilism dispute has a statement collaborators can check, by at least one of: its v2 propositions machine-checked with calibration defended as a fairness condition; a v3 with trembling-hand calibration grounded in learning; its open questions Q1 to Q12 answered or reformulated.

The tiling results for expected-utility agents using versions of UDT account for time and causality, so that an agent modifies only the parts of its policy causally downstream of the present, by at least one of: the causal-order formalization of the paper's theorems; a communication-based tiling theorem with a non-degenerate witness; a direct treatment of UDT 1.0's self-coordination.

A formal account says which updates an updateless agent accepts, what it is updateful about and what updateless about, so that an updateless agent can defer to a better-informed successor, by at least one of: a non-definitional deference relation on the canonical examples; the coupling-graph characterization of decision-flat refinements and its extension beyond pairwise coupling; a superconditioning bridge from endorsement to evidence-indexed policies.

Value uncertainty is separated formally from empirical and logical uncertainty, and a geometric aggregation across value hypotheses says how updateful an agent is about each, by at least one of: a deference theorem for the Geometric UDT construction under honest hypotheses; a bargaining rule weaker than Nash and Pareto for hypotheses without gains from trade; an explicit open-minded epistemic state with its own optimal-policy notion.

Updateless reasoning is derived from axioms about agency, correctly attributing unified agency to a system in a fair environment implying that the system's choices maximize policy utility, by at least one of: the approximate decision-determination bridge; a minimality premise restoring the agency correspondence.

Updateless agents coordinate with other agents by at least one of three routes, distributed cooperative oracles, Payor's lemma or higher-order game theory, or by a tiling statement for an agent inside a coalition; techniques may transfer between self-coordination and coordination with others.

The probability an agent assigns to an unrealized branch of a decision problem is anthropic uncertainty about its own location rather than a caring measure over branches fixed by its prior.

Total Trust, the notion of alignment in Deference Done Better, is an updateful notion: total trust and deference come apart when actions have acausal consequences.

An agent's optimal treatment of uncertainty is updateful about moral uncertainty, an aligned AI mostly or completely updateful about human values, and updateless about other matters.

The definition of optimality is part of the subject matter of decision theories, so arguments that decision theory is systematized winning need a notion of winning that presupposes no theory's optimality, and the decision-problems formal core supplies that notion through calibration of decision problems.

Once the evidence-partition assumption is dropped, observing one's own beliefs is the only notion of observation available to a logical inductor.

UDT over a Bayesian logical inductor pays in a single-instance counterfactual mugging whose two branches are correlated through its own later beliefs, by the decomposition argument the repository's BLI sources call the single-instance success thesis.

Under no-dependence of the policy, reflectivity and no cross-branch effect, the one-step UDT maximizer set equals the updateful maximizer set at every positive-mass table, with an epsilon form for approximate versions of the hypotheses.

A computationally uncertain UDT over a BLI on FAF's logical induction algorithm behaves updatefully on an observation branch whenever the policy condition has negligible effect on the other branches' expected utilities and on the branch probabilities, as an asymptotic theorem.

Exact reflection fails on FAF's diagonal liar at interval resolution, a logical inductor violates exact no-net-update and exact self-trust at day 1, and the propositionally coherent logical-induction criterion of Soto's 2023 notes is empty as printed.

The post-hoc transfer of large prices, the clamped re-pricing, full-scope faith for B1, coordinatewise rounding preserving coherence, and the modulus constant of the BLI sources are each refuted in Lean over FAF, in the readings the clean-room run chose.

UDT 1.1 behaves updatefully with respect to evidence exactly when the predictor's counterfactual reasoning is updateful with respect to it, in Versions A and B of the biased-coin counterfactual mugging.

At a recorded point, interventional supposition on the act equals conditioning on it if and only if the act is independent of its graph-parents under the state, so the CDT/EDT contest has no content there (Theorem 3 of the CDT-in-the-learning-setting note, four clauses).

The propositions of the maintainer's two-lesions document, the calibrated Smoking Lesion with its fixed points, dynamics and Proposition 5's bound, are machine-checked over the finite-tree semantics, with Proposition D as the formal home of recording the draw.

The bet extension of a decision problem and who buys it, the Definition-6 inversion on opaque Newcomb, Death in Damascus under both encodings, the existence of a mixed self-ratifying point by Kakutani, and the epsilon-fixed points are machine-checked over the finite-tree semantics.

In the finite shadow of a BLI prior, an agent that learns its policy over time and one that freezes it at the prior separate as Theorem A and Theorem B's learning half state, and two conjectures of Soto's 2023 notes are refuted.

The UDT 1.01 influence calculus of Posts 6 to 8 is formalized: Lemmas 1 and 2, Theorem 1 under the literal A5 profile with a construal-dependent counterexample, Theorem 2 as tiling, conservation of expected gain and the value of deferral.

Harmony between heterogeneous decision points is a trembling-hand equilibrium of a bargaining game; the source note's Theorem 11.1 is false at two players and Proposition S replaces it, with a harmonious optimum existing on the homogeneous game.

Geometric UDT selects an updateless policy as a Nash bargaining solution between value hypotheses with an updateful policy as the disagreement point, so that an agent uncertain about human values does no worse for any hypothesis than an updateful learner would, for a broad class of hypotheses.

Theorem 3 of Understanding Trust, UDT 1.1 Vingean tiling, has content under a non-naive reading of Faith in Joint Argmax, such as the computation-output model.

Every learner whose guarantee is optimality along every subsequence of decision problems fails policy-level optimality in counterlogical mugging, and a sharp impossibility theorem states this.

The decision-theory line aims at verdicts on the classical one-shot decision problems in addition to the asymptotic-average guarantees of the LI/BRIA minimum.

The weight an agent gives other branches of a decision problem decays as it learns, in contrast to UDT, where the weight is fixed by the prior.

The decision-problems formal core's optimality notion relates to tiling: a policy optimal in the formal core's sense tiles in the sense of the Understanding Trust results under stated conditions.

A Bayesian logical inductor can be read as a heuristic estimator whose arguments are of the form that the logical inductor thinks a sentence true, and broken down into finer arguments.

A formal model exhibits a trade-off between the generality of an agent's feedback, output-only against more general, and what it can learn, in the setting of Bayesian logical induction, the reflection principle and radical probabilism.

The BLI picture of computational updatelessness, future belief states as observations with constraints on large beliefs, can be improved until it reflects a computationally uncertain agent that observes its own future beliefs well.

The LI/BRIA acceptance statement with its updateless extension can be improved until it reflects a computable agent that learns policy-level behaviour well.

The decision-problems formal core, trees over decision points with calibrated subjective states, can be improved until it reflects an embedded agent facing decision problems with predictors well.

The Understanding Trust tiling framework can be improved until it reflects a self-modifying agent in time with computational uncertainty well.

The UDT representation-theorem framework, with decision-determination as its fairness axiom, can be improved until it reflects a system to which unified agency is correctly attributed well.

The decision-theory line's README lists, for collaborators, the decision-problems working notes, the clean-room BLI, UDT and decision-problems packages, and the two-lesions wiki copy under the clean-room sources.