The mathematics behind ArgMap

An argument map in this project is a probability model. The numbers a reader sees are the output of solving that model, not decoration on a diagram. This document explains what the model is, how it is solved, what has been proved about it, and what has not.

It is written for someone who is comfortable with probability but has never seen this project. No prior reading required. Where a claim rests on a derivation, the derivation is cited rather than reproduced, and §9 maps every citation to its home document.

One honesty note before the tags. The home documents and scripts this page cites live in the project's working repository, which is not yet public. A citation here therefore names the exact place a claim is checked; it is a record you can hold the project to, not a link you can follow today. What you can verify without the repository is the deployed app itself: the solved values and tension readings this document explains are computed live in your browser, on the shipped map, by the same kernel this page describes.

What the tags mean. Every quantitative claim below is either (a) proved, with a pointer to the proof, (b) measured, with a pointer to the script that reproduces it, (c) a constant the record chose and says so, or (d) explicitly open. The tags [proved], [measured], [standard], [convention] and [open] are used consistently and mean exactly that. Section 7 is the full ledger. Two results in this project's history were refuted, and both are stated below, in the places where a reader would otherwise assume the convenient thing. Every number tagged measured was re-run on the shipped solve on the date beside it; a number from the retired reference of §4.4 says so where it appears.

1. The one-paragraph version

A document declares statements (claims that can be true or false) and reasoning links (the format calls each one an evidence and writes it on one line; this page says link). Each carries a number the author asserts, and since 2026-09-08 (DECISIONS D161) each number has two axes: a value (how likely) and a count (how firmly it is held, in the currency of coin flips). The links, with their values, compile into a directed probability network, the map's own: each strengthed reasoning step is a coin at its authored rate, where an in-force step's premises hold its conclusion is forced, and where nothing forces a statement the network fills it at one half. The statements' values are targets on that network, each held with its count, and the solver picks the distribution closest to the network that meets the targets as well as they can jointly be met: an I-projection, computed by a ridge dual (our name for the L2-regularized maximum-entropy dual, the Gaussian-prior maxent model; SOLVER_FAQ-2026-07-14.md Q2 gives the standard references) over a junction tree. Every solved number a reader sees is a marginal of that one distribution, or the posterior rate of one coin. (Two restrictions are real and §3 states them: an undercutting link forces nothing, a link with no strength compiles to nothing, and a check credence is displayed without ever constraining the solve.) Where a support and an objection bear on the same case, their links are shares of one population: they never fire together, each keeps its authored rate, and the assumption that they are independent is what gives way (§3.8, D166). Where the author's numbers cannot all hold at once the solve does not fail: the targets are springs, the residual disagreement is shown, and the colour of a node means one thing only, that the solved value has left what its author wrote.

An argument map written by a human being will not be globally coherent, and that last property is what the construction is built for: local honesty is enough, and incoherence becomes a readout instead of an error.

2. Design constraints (why not something off the shelf)

The semantics was designed backwards from authorability. Each of the constraints that drove it rules out an otherwise-obvious choice:

1. Local elicitability. An author must be able to write a number for one reasoning step while looking only at that step, without holding the whole document in view. This is what makes a large map writable at all.
2. Survival. A number the author asserts should still be there after solving, unless something else in the document actively contradicts it. An author who writes 0.8 and reads back 0.8636 (the figure the material placement actually produces, measured below) has been silently overruled by bookkeeping.
3. Local honesty without global coherence. The author is never required to make the document consistent. Inconsistency is a legitimate end state.

Constraint 2 rules out two natural placements of the number. The "material implication" placement fails survival outright: on the base case an authored strength of 0.8 reads back as an achieved conditional P(c|a) = 0.8636 [measured] (toy_run.py, case "T2 material hard (regression)", verified 2026-08-11). And a rule-activation prior left to float with the rest of the model makes the achieved conditional depend on everything else, so no document-local number yields a fixed authored conditional [proved] (Prop A8, SOLVER_PROOFS §4.8). Under the shipped model the rate IS a prior on the step's coin, and it survives for a reason Prop A8's hypothesis excludes: a count row holds the coin at its authored rate with the link's count (§3.2), so the rate is a soft claim the solve honours rather than a free parameter it re-estimates. Prop A8's "cannot survive solving" is a statement about the unheld prior, and it still holds of that.

Existing frameworks each give up one of the three. Abstract argumentation (Dung; Pollock) has defeat structure but no calibrated uncertainty. Probabilistic logic programming (Sato's distribution semantics, ProbLog) does give each rule a local number, as a switch prior, which is the unheld placement just described. Markov logic networks fail constraint 1 instead: a learned weight is globally normalized and has no document-local meaning. Probabilistic argumentation (Hunter, Thimm) typically stops at abstract graphs. Bayesian networks are the nearest neighbour on the model side, and since D161 the map's reference IS one (§3.1): what a Bayesian network lacks is the second half, a way to hold an author's number on a derived node as a soft claim beside the network's own value, which is what the targets and their counts add. The nearest neighbour on the authoring side is probabilistic conditional logic under maximum entropy (Paris 1994; Kern-Isberner 1998, 2001; the SPIRIT and MEcore systems, Rödder et al. 2006, Finthammer et al. 2009; survey: Kern-Isberner, Beierle, Finthammer, Thimm 2011): one conditional with one number as the authoring unit, and an I-projection as the solve. It gives up constraint 3: a conditional there is a hard constraint P(ψ|φ) = d, so the model exists only for consistent knowledge bases, and its number is the conditional probability rather than the inference's reliability (a d below one half is a low conditional there and a weak support here; ideas/plans/semantics-prior-art-kern-isberner-2026-08-31.md §4 carries the translation rule). What is new here is the contract, and the specific compile that satisfies it: the map's own network as the prior, the authored numbers as soft targets with counts, kept well-defined on contradictory maps by the penalty of §4.2.

3. The model

3.1 Worlds, the reference, and the completion principle

The solver works over a joint truth table whose coordinates are the statement variables plus one coin E₀ for every evidence line that carries a strength and a premise (plus compile-internal auxiliaries for undercuts and refinements). A coin is read as "this rule is in force": a world where E₀ holds is a world where that inference actually carries. Making in-force-ness a random variable, rather than a property of the graph, is what lets a reasoning step be probabilistic without being a mere correlation.

The reference the solve starts from is the map's own network (D159, adopted 2026-09-03; shipped by D161, 2026-09-08; GLOSSARY network reference): the statements are grouped into blocks (strongly connected components merged with co-conclusion clusters), and a world's reference mass is, per block, the uniform mass divided by the number of the block's joint values alive under the lines' zero-sets. On the acyclic fragment that is a Bayesian network with uniform fill-ins: P₀(s | parents) = 1 where an in-force line with true premises concludes into s, and ½ otherwise, with each coin's authored rate as its own prior factor. Two things follow at once and are measured in §5: the free antecedent of a lone implication reads 0.5 exactly, and a derived statement reads what its in-force lines deliver.

Every authored construct compiles to one or more of:

• structural zeros: worlds deleted outright;
• prior factors: a coin's rate, the block reference;
• targets: soft rows on the solved distribution, each with a weight derived from its count.

The completion principle is the frame the reference was chosen in (Felix, 2026-08-28; ideas/plans/semantics-bookkeeping-hull-2026-08-28.md section 6, and the project's norm for every new semantics decision since). Every authored number is a marginal or a conditional of ONE complete distribution the map only partly writes down: a statement's pin is the zeroth-order piece, marginalized over everything; a one-premise line the first order; a two-premise line the second. Authoring a node conjures the whole completed structure around it, every expressible sibling at a default value, and the compile is the residue after everything that provably cancels is removed. The question the reference answers is which shape the defaults take: every joint cell at ½ (the uniform counting reference, §4.4) or every unauthored conditional row at ½ along the map's own given-bar direction (the network reference). The two completions differ on exactly one visible thing, the antecedent pull of §4.4, and the network shape is the one whose fingerprint agrees with Bayes (§5, §7).

3.2 Evidence lines: coins with a kind

A support line $E p ψ | π ("ψ, given π, with strength p") compiles to three things (two carve-outs follow: an undercutting line gets no zero-set, §3.4, and a line with no strength compiles to nothing at all, being display-only):

1. a coin E₀ at prior rate p, a unary factor; an authored 1 is a fact, no coin, a pure zero-set;
2. the zero-set: worlds satisfying E_eff ∧ π ∧ ¬ψ are structurally dead. Where the rule is in force and its premises hold, worlds contradicting its conclusion do not exist. (E_eff is the effective in-force variable of §3.4; absent any undercut it is just E₀.)
3. a count row: P(E₀) = p held at weight n / (p (1 − p)), n the line's count in flips, so that a line holding n flips resists a change of its rate like n Bernoulli observations at that rate would. This is the only constraint a line contributes; the mirror rows of the retired reference (§4.4) left the constraint set with D161.

The number is a floor, not a point value. This is the most consequential thing to understand about reading a solved map. The line guarantees its conclusion at least this much and says nothing about the rest: where the rule is in force the conclusion holds, and in the remaining worlds the line is silent. The network fills that silence at ½, so the achieved conditional lands above the authored strength, at p + (1 − p)·½ in the base case: 0.9 for an authored 0.8. This is the F1 fill identity [proved] (SOLVER_PROOFS §6.8; unchanged by the change of reference, because the fill is the reference's own, and re-measured under it in §5). Nothing has been overruled: the coin is in force in exactly the fraction of worlds the author wrote. And evidence can accumulate: two independent lines for the same claim add up by noisy-OR, where a point value would have one cap the other. Where an objection bites in the same case, the lines are shares of one population instead, and §3.8 says how they combine.

The line's count comes from its kind (D161 item 3 and its appendix, the first ruled table; revisable by amendment when a map's acceptance tests say so). The kind is a comment key on the line, # kind: <word>, read off the source's own words, and it is content: it ports 1:1 to a translation. The table, in flips:

The solve reads four counted tiers (1000, 64, 16, 4) and the hard one, so a disagreement between empirical and testimony, or between analogy and hope, moves no number. The constants are [convention]: K2's 64 is continuity with the weight the flagship was authored under (a w = 400 pin at 0.8 was 64 flips), the tiers below it are ratios of four fixed so that a hope tends to bend before an analogy before a mechanism (a tendency by count, never a rule by position: only numbers on the path between a reader's claim and the case's roots can give), and K1b's 1000 is the campaign's amendment A1 of the ruling's 200: at 200, the point cap of §3.3, a quoted deductive line beside two point premises bent with them, and the rationale is now "firmer than any statement a point can be, and softer than a formal step". An undercut takes the kind of its own step, never the kind of the line it attacks.

Measured at the ruled tier, through the shipped compile and the WASM kernel (2026-09-08, D161 item 3; solver-compile/tests/socrates-tier.test.ts pins it as a dated fence). On the confusions map's two-premise Socrates syllogism, both premises at 0.99 and the reader's "not mortal" at 0: formal holds 0.990 while the premises give (0.99 to 0.667 each) and the reader is refused (0.323 against 0); deductive at 1000 reads 0.930, the premises 0.687, the reader 0.303, and the single-premise copy 0.986. The condition the raise was set for (the coin above 0.95 while the premises give) is met by formal and missed by deductive by 0.02 on the two-premise copy; the ladder reads 0.750 / 0.930 / 0.959 / 0.977 / 0.987 at 200 / 1000 / 2000 / 5000 / 20000 flips. The constant stands and the miss is on the record for a ruling.

Kind is content, and it was classified like the values. Two blind passes over the flagship's 348 strengthed lines from the rubric text agreed on 251 (0.721; Cohen's kappa 0.651 against chance 0.201), and a third blind reader broke the 68 ties (D161 appendix item 10). The adjudicated keys on the map, recounted 2026-09-08 by grep: 105 mechanism, 69 deductive, 65 testimony, 45 hope, 34 empirical, 30 analogy, no formal. Since 2026-09-26 two lines carry formal, the analytic inverses $not-feasible-not-built and $no-win-no-extinction at 0.99 (the phone walk's ruling F2, true by the meaning of their terms); the same day's grep recount reads 106 mechanism, 69 testimony, 66 deductive, 48 hope, 35 empirical, 31 analogy, 2 formal. Since 2026-09-27 $harmless-no-extinction is formal too, and since 2026-10-06 $link-fine, the title claim's last step, both by the meaning of their terms; the recount of 2026-10-07 (grep over the strengthed lines) reads 106 mechanism, 69 testimony, 67 deductive, 48 hope, 35 empirical, 31 analogy, 4 formal. Since 2026-10-13 $built-grown, that a superintelligence built with today's techniques is grown, is a fifth formal line, by the meaning of its terms, and its partner $unbuilt-grown an empirical one; that day's recount (the same grep) reads 106 mechanism, 69 testimony, 67 deductive, 48 hope, 36 empirical, 31 analogy, 5 formal. One line in four got its kind by a judgment call, and a tier is a factor of four in flips; §8 says what that costs.

3.3 Statements: targets with a width-derived count

A statement's authored credence is a pair @s p⁺/p⁻ (D52): p⁺ is the mass the author commits to the statement, p⁻ to its negation, and m = 1 − p⁺ − p⁻ is the silent mass the author declines to place. Under D161 a pair compiles to one target, a row on P(s) at the mixture point p⁺ + m·R(s), where R(s) is the network's own value of s: the author's committed mass, plus the reference's fill of what was left open. A bare point @s p is the coinciding pair, m = 0. On the flagship's 224 pairs every solved marginal sits inside its interval [p⁺, 1 − p⁻] [measured] (2026-09-08 through the compile and the kernel, g-flagship.test.ts; the python route agrees). The alternative, a target allowed to sit anywhere in the interval, was measured and declined: on the same 224 pairs it clips 139 down to p⁺ and 80 up to 1 − p⁻ and moves 207 statements, where the mixture moves 12 (G plan ledger 23, 2026-09-07, a probe).

The statement's count comes from its width (D161 item 2). Walley's imprecise Dirichlet model [standard] (Walley 1996) reads an interval of silent mass m as n = s (1 − m) / m equivalent observations, with s = 2 the prior strength: a 0.7/0.1 pair (m = 0.2) holds 8 flips, a 0.85/0.05 pair (m = 0.1) holds 18, a 0/0.95 pair 38, and a point is read as a pair of silent mass 0.01, 198 flips, the point cap. The cap is count-only (amendment A6): a point stays a point target at its value, the cap sets its weight, and no target moves to a mixture point. The cap is what keeps the compromise of §4.2 alive (no point can make the solve infeasible) and bounds the curvature, so an authored 0 or 1 gets a large finite weight. Both s = 2 and the 0.01 cap are [convention]. The count enters the compile as the per-row weight it already carried, w = n / (p (1 − p)), so a pin at the old w = 400 was already 64 flips at p = 0.8, 36 at 0.9, 100 at 0.5.

On the flagship, recounted 2026-09-08 from argmap-query pinned-roots (224 pairs, no bare point): the rule gives median 18 flips, minimum 0.5, maximum 38 (one pair, @c5-boring 0/0.95); 168 pairs sit at 18, 27 at 8, 25 at 4.67, 3 at 0.5; 55 of the 224 sit below a bare line's 16 (recounted 2026-10-13 the same way: 236 pairs, no bare point, the same median, minimum and maximum; 179 at 18, 26 at 8, 26 at 4.67, 4 at 0.5, 56 below 16; on 2026-10-07, before @grown's pin became a check, 237 pairs and 180 at 18), and every mechanism (64) and every quoted deductive line (1000) is stiffer than every statement on the map. So under a reader's what-if the authors' own assertions give before their mechanisms do, which is the completion principle's order: a line holds more of the background fixed than a pin.

The two axes are different things: the pair's width says how much the author declines to commit, the count how much it takes to move the author. A claim can be imprecise but firm, or precise but fragile.

Two further slots keep their jobs:

• The check credence is the author's all-things-considered number, displayed against the computed posterior but never constraining the solve. It is how a map can say "the argument delivers 0.7, and I believe 0.9" without one silently overwriting the other. Since 2026-08-23 it is an interval, # check: 0.85..0.95, the range the authors' register licenses, and the displayed badge is the signed distance from the computed value to that interval, zero inside it. The flagship carries 67 statements with a # check: key on their head line (grep, 2026-10-13; 66 on 2026-10-07 and 2026-09-27, 64 on 2026-09-23, 60 on 2026-09-11, an earlier count of 63 read wrapped gloss lines too), and under the shipped solve one of them badges past 0.10, the headline @everyone-dies: 0.624 against 0.75..0.95, short by 0.126, the widest gap; the next is @fragile at 0.796, short by 0.054, then its third premise @mis-ext, 0.797 against 0.85..0.95, short by 0.053 (solve_map.py --top 1200 --badge-threshold 0.01, 2026-10-13, on the map with that day's grown line; 0.609 and 0.779, short by 0.141 and 0.071, @fragile third, on 2026-10-07, with $link-fine at 0.99 by the meaning of its terms since 2026-10-06; 0.591 and 0.779 on 2026-09-29, when $uc-precedented's strength was re-derived under the rubric, 0.3 to 0.5). On 2026-09-28, the evening, with the undercut-kinds pass (D170: the two objections that deny @mis-ext became lines against it, and the record one of them starts from, @precedented, was re-read as the fact the book grants), the headline read 0.603, short by 0.147, and @mis-ext 0.795, short by 0.055, a hair ahead of @fragile at 0.796. On 2026-09-27, the evening, with the aligned-inverse batch (D168: two inverse lines on the title claim priced the worlds the reference had filled at one half, about 9 points of the old reading), the headline read 0.617, short by 0.133, and the next was @fragile, short by 0.054. That morning none badged: the widest gap was @fragile's and the headline read 0.708, short by 0.042, on the map as restructured on 2026-09-25, when an audit re-read six checks from the sentences that price each claim's own quantity, the headline's 0.88..0.98 among them; on 2026-09-23 the widest gap was the headline's, 0.796 against 0.88..0.98, and on 2026-09-11 0.827 against it (§7 rows 4 and 12). The last badge standing was @evo-analogy at 0.417, and the 2026-09-08 evening pass closed it by mapping the chapter's own case for the analogy, which no number moved: 0.858 against 0.75..0.95.
• The balancing prior of the ratified D36 model, the engine's choice of a point inside an authored interval, is no longer a separate slot: the interior point of an interval is the network's own value restricted to it, which is what the mixture point says. Earlier editions of this page listed it as the largest open item on the authoring side; §7 lists it among what closed.

Pairs are authored under a residual rule: a statement's own mass should be evidence not already present elsewhere in the map, since double-counting the same consideration is exactly what the accumulation machinery assumes away. Frontier roots are exempt: their residual mass is the map's interface to the unmapped world.

Premise-less strengthed lines ($E p ψ, a floor with no given bar) are [open] (S18, D161 item 9): the placeholder reads them as targets [p, 1] on the conclusion that pool with their neighbours, which is the reading the one author we have sides with (he-xrisk's check 0.85 met at 0.837 at the K3 default), and a lint note names the placeholder on every such line. No comprehensive map carries one.

3.4 Undercuts: attacking the inference itself

An objection can attack a claim, or it can attack a step, which is Pollock's undercutting defeat. The latter is first-class here, because evidence lines are nodes and can therefore be referenced.

A line whose premises carry $X as a top-level positive conjunct and whose conclusion is the negation of X's conclusion (up to double-negation normalization) is the inhibitor of X, provided exactly one referenced line matches. Near-misses stay ordinary evidence: $X nested under an OR, a conclusion that misses the negation, or an ambiguous line matching two targets all compile as ordinary evidence lines, with flagging left to lint (the shape rule is SOLVER_FACTORED_UNDERCUT §1.1). Effective in-force is then defined recursively over the (acyclic) reference graph:

E_eff(X) = E₀_X ∧ ⋀ ¬( γ_L ∧ E_eff(L) )    over all L inhibiting X

where γ_L is the inhibitor's remaining premises (its guard). Inhibitors carry no zero-set of their own; an inhibitor's coin holds its own operative rate P(U₀) = q′ with its own count. The target's authored rate stays exactly where §3.2 put it: the count row holds the base coin E₀, untouched by defeat, and only the zero-set rides E_eff. An undercut therefore never rewrites the author's claim about the rule's in-force rate; its entire effect is to exempt guard-worlds from the target's zero-set.

Two structural properties fall out. Undercuts-of-undercuts (reinstatement, in the argumentation literature's sense) are just the recursion, with no new machinery. And defeat only ever revives worlds that the target's zero-set had killed. It never kills new ones. This world-revival principle makes a class of pathology impossible by construction rather than by check. The shape is D36's factored-A cascade, unchanged by D161; what changed is the readout: an undercut's coin has a posterior in-force rate like any line, and under a what-if that posterior against the authored rate is the loud row (on the flagship's P6 what-if set the testimony undercut $uc-experts reads 0.542 against its authored 0.30, §3.6).

Strength q′ = 1 is exact in-context elimination (immediate from E_eff = E₀ ∧ ¬(γ∧U)), and q′ = 0 is exactly inert in the hard limit. The behaviour between them is monotone [proved for the flat form under the ratified compile], with the general-graph statement [open] (D1, SOLVER_PROOFS §7.1, and see §7 for the refutation this claim survived).

3.5 Refinement: the same argument at two grains

A reasoning step can be refined, replaced by a finer subgraph that says how it works. The maximally-unfolded map is the canonical model; only leaf evidences carry coins (V8, "refinement replaces", D158). A refined line's in-force variable is defined by its delivery function: whether the refinement's own lines, composed, actually deliver the conclusion.

The consequences, all [proved] (SOLVER_PROOFS §8):

• Folding and unfolding are a readout, never a re-solve. Every folded quantity is a marginal of the same joint distribution, so the numbers cannot change just because a reader collapsed a box (R3).
• Coarse and fine agree structurally; only their numbers can disagree.
• An authored coarse strength on a refined line is not a solve input at all. It compiles as a zero-force spectator observable (D38).

What the folded line shows is open (S21, D161 item 9). The folded readout since 2026-09-08 is D51's composition: the refinement's own lines composed along its spine, marked apart by the dashed arrow ⇢ in its readout pair (beside the unfold + it shares with statements) and, since 2026-09-12, tinted against its authored point like any other row (D38, amended 2026-09-12: only the display half of S21 closed), on every strengthed refined line the compile can compose (the flagship's nine folded lines, e.g. $link authored 0.93, composition 0.675 on 2026-10-13, with that day's grown line (0.658 on 2026-10-07, since $link-fine reads 0.99; 0.618 on 2026-09-29, 0.630 on 2026-09-28, 0.638 on 2026-09-27); 0.765 on 2026-09-08, and 0.856 until the interior premises counted, later that day, below). The obvious alternative, the whole-network conditional P(conclusion | premises) through the block, was ruled and then reopened the same day (amendment A3), because it reads the conclusion's other parents: on the flagship $resp-waitshot came out at 0.9951, which is @shutdown's marginal, and six of the eight measurable refined lines sat more than 0.05 off their authored strength on the untouched map [measured, 2026-09-08]. That conditional stays a bench observable until a block-local definition exists. The composition reads a refinement recursively: a chain's steps multiply, a convergent group's routes OR, and a fan is the final step AND (any one route with its own interior); the implementation had closed the spine flat until 2026-09-08 (every route's interior at once), which read 0.512 on the flagship's $resp-waitshot where the recursion reads 0.900 against its authored 0.90 [measured, 2026-09-08, W5-A; anchor examples/toys/c-fan.argmap]. What remains open is the product: four steps that are all required multiply to $c5v-resp 0.516 (0.9 x 0.9 x 0.85 x 0.75) on a 0.90 line, and whether that product is the line's own number is S21's remaining question. The composition counts what its steps rest on (W5-G, later on 2026-09-08). A step's coin being on says nothing about whether the step's premise holds, and the event was built from the coins alone, so a hope objection counted as delivering at its full rate beside its own premise at 0.17 ($hope-care 0.673 against 0.15 authored). The readout now reads the DELIVERING event: the coins AND every premise the steps need that nothing inside the refinement delivers, at its posterior, given the coarse line's own premises; what a reference to the line denotes is unchanged (the coins in force), so no marginal moved [measured, 2026-09-08, W5-G: 343 files, both references, max 3.8e-8; anchor examples/toys/c-interior.argmap]. On the flagship: $link 0.856 to 0.765, $hope-care 0.673 to 0.290, $hope-useful 0.220 to 0.074, $hope-harmless 0.243 to 0.245, $hope-design 0.409 to 0.046, $c5-promise-resp 0.810 to 0.644, $resp-waitshot 0.900 to 0.894, $c5v-resp 0.516 to 0.270 (the product times the four steps' own premises), $shutdown-ev 0.864 to 0.777 [measured, 2026-09-08, solve_map.py at the default]. Whether this conditional is the block-local definition is S21's question in its remaining form: it reads the refinement's own event, but its interior at the whole joint's posteriors. Under G without counts the parallel-leaf ladder of P9 is flat (0.1122 at one to four leaves); with counts it returns in proportion to the count, which is S19 (§7).

3.6 The reader's what-if: revision

A reader who moves a statement's number enters it as a point at the point cap, 198 flips, the same rule as an author's point (amendment A2; a reader's 0 or 1 is a point at the cap, never a fact), and it REPLACES the author's number on that statement (fork 4). Two cases follow (D161 item 4 as amended 2026-09-08; the tutorial's 4.6 teaches both with these numbers):

• On a pinned root, nothing bends and the map follows the reader forward. @llm-nice (the authors' 0.85?/0.05? that current systems seem nice; consumed by two lines, concluded into by none) moved to 0.1: as authored it read 0.877; under the reader's number it reads 0.101, a residual of 0.001 below the tint's tolerance, so nothing colours; the one downstream statement moves (@nat-abs 0.194 to 0.103), the headline stays at 0.827, and no coin sits more than 0.05 from its authored rate [measured] (2026-09-08 through the compile and the kernel, solver-compile/tests/root-whatif.test.ts; solve_map.py --override llm-nice=0.1 agrees). Under the one draw (§3.8; solve_map.py --cell-draw chain, 2026-09-23) the same what-if reads @llm-nice 0.881 as authored and 0.101 under the reader's number, @nat-abs 0.202 to 0.108, the headline at 0.796 before and after; re-measured 2026-09-27 on the map as restructured on 2026-09-25, the four numbers read the same and the headline 0.708 before and after; the same evening, with the aligned-inverse batch (D168), the four numbers again read the same and the headline 0.617 before and after; on 2026-09-28, with the undercut-kinds pass (D170), the headline reads 0.603 before and after (root-whatif.test.ts through the kernel); on 2026-10-07 the four numbers read the same again and the headline 0.609 before and after, nothing else moving past 0.01 (solve_map.py --override llm-nice=0.1 over every node), and on 2026-10-13, with the grown line, the same four and nothing else past 0.01, the headline 0.624 before and after (the same command).
• On a derived statement, the author's case retreats where it is softest. The reader's number is one more target beside the author's, the map re-solves, and what bends shows what the case holds least firmly: under the counts a hope tends to bend before a mechanism, a formal step never, the authors' own deductive claims last. On the flagship's P6 set (built, misaligned when built, the misalignment extreme, the link fine, and still nobody dies), the reader's points are met to 0.002 (@everyone-dies 0.0020, @if-built 0.9981, @mis-ext 0.9982), and the retreat lands on the analogy response $resp-exp 0.90 to 0.632, the testimony undercut $uc-experts 0.30 to 0.542, the analogy undercut $uc-precedented 0.30 to 0.351 and one mechanism, $c12dr-obj 0.15 to 0.205; no deductive coin bends [measured] (2026-09-08 through the compile and the kernel, D161 item 4, g-flagship.test.ts). Since 2026-09-28 (D170) the two objections that deny @mis-ext are lines against it rather than undercuts of $link-fine, and the retreat has one undercut left to bend: in the same compile the points are met to 0.005 (@everyone-dies 0.0044, @if-built 0.9956, @mis-ext 0.9956), the testimony doubt $uc-experts goes 0.30 to 0.982 and $resp-exp 0.90 to 0.273, and no mechanism coin bends ($c12dr-obj 0.150, $uc-precedented 0.286) [measured, 2026-09-28, g-flagship.test.ts]. Since 2026-09-29 $uc-precedented carries 0.5 and reads 0.479 under the set, 0.021 under its strength; the other figures hold (the same file, re-read 2026-10-06; $link-fine is one of the set's own points, so its ruling of that day moves none of them). The walkthrough's beat is this case too: the lemma @asi-soon (since 2026-09-25 the claim that a machine superintelligence can be built; check-only, 16 lines conclude into it) set to 0.1 reads 0.149, 0.049 refused and tinted, with @everyone-dies following 0.624 to 0.136 and @if-built 0.835 to 0.140 [measured] (solve_map.py --override asi-soon=0.1, 2026-10-13, with the grown line; 0.609 to 0.133 and 0.836 to 0.140 on 2026-10-07; 0.591 to 0.130 on 2026-09-29; 0.603 to 0.132 on 2026-09-28, the evening, with the undercut-kinds pass, D170; 0.617 to 0.136 on 2026-09-27, the evening, with the aligned-inverse batch; 0.708 to 0.160 that morning; the editor's walkthrough.test.ts pins the same three through the kernel). On 2026-09-08, before the one draw and the restructure, the beat read 0.124, with the headline 0.827 to 0.523 and @if-built 0.910 to 0.555. Under the one draw (2026-09-23) the P6 set's numbers above read the same to three decimals, and they still do on the map as restructured and with the aligned-inverse batch (2026-09-27; @mis-ext 0.9982 to 0.9981, the same three decimals); the D170 figures above read the same to three decimals under the one draw too (solve_map.py at its default with the P6 overrides, 2026-09-28), and still do on 2026-10-07 and on 2026-10-13, $uc-precedented at 0.479 (the same command).

Where the map cannot honour the reader's number, the residual is shown and the row colours past the tolerance of §4.3. The other verb, conditioning (the reader's number as a fact on the author's solved joint; the premises move by Bayes and no line ever gives), answers a different question, "suppose it turned out that way", and differs from revision by 0.5 on the reader's toy (s05: 0.2814 against 0.7910, PLACEMENT_PROBE 20.2, a probe); it stays a bench verb (solve_map.py --condition) and the candidate for a binary mode.

3.7 Explaining away, declared

Two causes of one known effect become dependent in a probabilistic network, and the map, being one, shows it: with only the effect observed both causes rise together, and observing one of them as well lowers the other, because the effect is already accounted for. On the exhibit examples/toys/f-explaining-away.argmap (two causes each bringing the effect at 0.9; in the app, the Semantics audit map audit-forks, group F6) the effect alone puts each cause at 0.573, and observing one cause drops the other to 0.515 [measured] (solve_map.py at the default, 2026-09-08; the record's hard-mode figure is 0.5116, against the 0.6552 the conditional-logic literature's syntax-splitting postulate (CInd) would demand). D161 item 6 declares the divergence: the network reference satisfies syntax splitting's (Rel) and (Ind) exactly and (CInd) on fork and chain pivots, and fails (CInd) on a collider pivot by exactly this. (CInd) is not a property the map claims. Under the retired uniform reference the same toy read 0.496 and 0.498: no explaining away at all, which is one more face of the antecedent pull.

3.8 Lines that meet in one case: one draw (D166, ratified with the one-draw release, 2026-09-23)

A line's number is a rate of cases: $E 0.85 ψ | π says that among the worlds where π holds, the line makes ψ true in at least 85 of every hundred. That is the rubric's question, P(conclusion | premises). When several lines bear on one statement, the worlds split into cells, one per joint assignment of their premises, and in each cell the lines that bite (premise true, not defeated by their own undercut, §3.4) are shares of one population. Their firing is decided jointly, in one draw, under three rules in priority order:

1. logic never gives: a line for ψ and a line against it never fire in the same world, since ψ would be both true and false there;
2. the authors' rates hold: each line fires in its stated share;
3. independence is the default and gives first: beyond 1 and 2 the draw is the maximum-entropy one, assuming nothing else.

Everything else follows from these three rules. Where only one side bites, the lines are independent and accumulate by noisy-OR (§3.2): more reasons, more confident, never certain. Where a support at s and an objection at t both bite and s + t ≤ 1, each keeps its share: 0.85 against 0.15 reads 0.85 in that cell, with nothing contradicted. Several supports against one objection nest inside the strongest of them and count as much as it does: in the cell where all their grounds hold, five supports at 0.9 against an objection at 0.15 read 0.895, the same as one (0.9 and 0.15 pass one by 0.05, so that number is the ratio rule below). Where the strongest rates pass one, the numbers disagree: the overlap s + t − 1 is dead mass, killed by the zero-set, and the cell reads the ratio of what each side holds uncontested, (1 − t) : (1 − s); 0.9 against 0.7 reads 0.75 with 0.6 dead. The dead mass lowers the weight of the cell whose lines clash, so the pressure lands on the grounds that produce the clash, continuously: at strength one the combination is impossible, below one it is made rare. The number of lines never outvotes the other side; an answer to the objection (an undercut), a lower number, or doubt about its grounds does.

The alternative it replaces is evidence weighing. Until D166 the solve drew every line as an independent coin and deleted the worlds where a support and an objection both fired. In one cell that is exactly noisy-OR within each side and likelihood-ratio multiplication across sides, the Bayesian reader's instinct for independent evidence [proved] (the identity is algebraic at the reference's ½, written out in §7). Under the rate reading it breaks the authors' own sentences: 0.85 against 0.15, numbers that fit exactly, read 0.901, because the deleted worlds are mostly the objection's. On the flagship the book answers almost every objection it raises, so the change is modest: 19 of its claims move by 0.01 to 0.04, @shutdown from 0.999 to 0.957 and the headline @everyone-dies from 0.827 to 0.796. Of the 64 claims the book gives a range for, 15 sit outside it by more than 0.01 against 19 under evidence weighing; seven of the moves go toward the book's range and one away from it, the headline's, which already sat below the 0.88 to 0.98 it was then checked against [measured, 2026-09-23, the compile and the kernel, the python oracle agreeing to 5.5e-8**]. On the map as restructured on 2026-09-25 (§3.3) the same comparison reads the headline 0.708 against 0.726 under evidence weighing and @shutdown 0.952 against 0.992, and of its 66 checked claims 17 sit outside their range by more than 0.01 against 21 [measured, 2026-09-27, solve_map.py at the default and at --cell-draw off]; with the aligned-inverse batch the same evening (D168) it reads the headline 0.617 against 0.641 and @shutdown 0.928 against 0.961, the misses 17 against 21 still, and the headline the one badge past 0.10 under both [measured, the same two commands]; with the undercut-kinds pass (D170, 2026-09-28) the headline 0.603 against 0.630 and @shutdown 0.928 against 0.961 [measured, the same two commands]; on 2026-10-07, with $link-fine at 0.99 since the day before, the headline 0.609 against 0.636 and @shutdown 0.928 against 0.961, the misses 18 against 21, and the headline still the one badge past 0.10 under both [measured, the same two commands]; on 2026-10-13, with the grown line, the headline 0.624 against 0.651 and @shutdown 0.929 against 0.962, the misses 18 of 67 against 23; the headline is the one badge past 0.10 under the one draw, and under evidence weighing nothing badges past 0.10, the headline 0.099 short [measured, the same two commands]**.

The one assumption is the even spread: a line's rate holds across all of its cases, including those where another line's grounds hold too. An author who disagrees names the statement that separates the two lines' cases, and the lines stop meeting in one cell.

Computing it. A block whose per-cell table has at most 16 variables is drawn exactly; a wider one by a chain over its lines sorted by rate (D166 item 5), exact wherever the strongest rates reach one [proved] and within 0.001 of the exact draw per flagship block where they fit [measured] (§7 has both; §6 has what the chain costs). Premise-less lines keep the bound reading of D161 fork 2 until after the release (D166 item 4).

4. The solve

4.1 The I-projection

Given the network prior R (§3.1) and the targets, the solver picks the distribution Q that minimizes KL(Q ‖ R) plus the targets' penalties: the I-projection of the reference onto the author's claims. In hard mode (the targets exact) this is Jeffrey's rule for several marginals at once (Williams 1980 [standard]), and it reports INFEASIBLE rather than a number where pins meet zero-sets. For inference from a consistent set of constraints, minimum cross-entropy is characterized axiomatically as the unique rule meeting a short list of consistency requirements [standard] (Shore & Johnson, IEEE Trans. Inf. Theory 26(1), 1980; Paris & Vencovská, Int. J. Approx. Reasoning 4, 1990); the earlier edition of this page invoked the same result with the uniform counting measure as R, and what D161 changed is R, not the projection. Picking some other member of the feasible set requires a reason the document does not contain. Two caveats: the Shore and Johnson axioms have been contested and refined in the later literature, and the characterization is for the consistent case, while the default solve is the penalized relaxation of §4.2, which is where inconsistent documents actually land.

Accounting is F1: the divergence is measured over the full joint, coins included. Quotient variants that measure only over statements were implemented and are retired to comparison oracles.

4.2 Two modes, and why the penalized one is the default

Authored numbers frequently cannot all hold at once. The minimal case is two conclusive evidences for opposite conclusions. There are two modes:

• Hard: targets exact. Infeasible sets are then genuinely infeasible, and the dual problem has no stationary point. The failure is abrupt: on a family of opposing floors with feasibility gap γ, the exact dual's multipliers grow like ln(C/γ) and its Hessian conditioning like Θ(1/γ), diverging as the gap closes [proved, with the constants derived] (Prop B5, SOLVER_PROOFS §5.5).

• Ridge (the default): each target gets a weight w, and the problem becomes a quadratic-penalized projection whose Fenchel dual is a ridge-regularized log-partition minimization,

  min_λ  log Z(λ) + Σᵢ λᵢ² / (2wᵢ)
  

  with ln R folded into the static potentials, multipliers bounded by construction and the solution smooth (C^∞) in the authored numbers, straight through the point where the hard problem breaks [proved] (B1, B3, B4, B5; the reference term changes the potentials, not the duality).

What the ridge penalizes deserves one more line, because it is where a reader first meets the solver's arithmetic. The penalty is on each row's moment residual, (w/2)·(E[g] − p·E[h])²; for a target on a statement (h ≡ 1) that is (w/2)·(q − p)², the residual a reader would write. The weight is the count: w = n / (p (1 − p)), so that for small moves the penalty is n·KL(p ‖ q), the price n coin flips at rate p put on a rate q [standard]. What the old single corpus weight (w = 400 for everything) became is therefore not a knob but a table: 198 flips on a point, the Walley count on a pair, the kind's count on a line. Scaling every count by one constant is a temperature against the reference term and not an invariance (on the reader's toy s05, with the reader scaled too, a reads 0.5312 at c = 1/16, 0.5272 at 1, 0.5268 at 1024, PLACEMENT_PROBE 20.2, a probe); what is not saturated is the ratio of counts between the parties to a conflict, which is why the counts are content.

This is the mathematical content of "incoherence is a readout". The penalized problem is always solvable, and conflicting authored numbers produce a compromise plus a per-row residual rather than a failure. The two modes are continuously connected: as the counts grow the penalized solution converges to the hard projection when one exists, and otherwise to the projection's point among the minimizers of the violation functional [proved] (Thm B6, §5.6). So the default is a principled relaxation of the exact problem, and not a different problem.

One price of the retired reference closed with it. Under the mirror rows of §4.4 a conditional row over a thin slab of mass P(φ) was penalized by P(φ)², so a rule over a branch of mass 0.01 could rest 0.24 from its authored value for a penalty near 1e-3 (P7, "the thin-slab price"). With no conditional rows in the constraint set the price has no subject: on the flagship $bounded-escape reads 0.900 against its authored 0.90, where under the retired reference the same line's premise-side row sat at 0.378 [measured] (solve_map.py at the default and at --reference d36, 2026-09-08; D161 item 7 quotes 0.193 for the kernel's effective in-force readout of the same line under the retired reference).

4.3 Tension: the set rule

A statement or line colours only where the solved value has left its authored set (D161 item 5, fork 10): below a floor's value, outside a pair's interval [p⁺, 1 − p⁻], off a point. Tension is the distance from the solved value to that set, zero inside it and below a tolerance of 0.01 (amendment A7, the ridge's own residual at a point: a point at the cap solves about 0.005 off). Inside the set there is no conflict, only the solve filling what the author left open, and that stays visible as a readout (the gauge's fill, a coin's posterior) without colour. On the flagship as authored no pin and no coin tints (224 of 224 pairs inside their intervals, every coin within 0.05 of its rate, 2026-09-08; 237 of 237 pairs and every coin within 0.03 on 2026-09-27, and again on 2026-10-07, the farthest coin $nat-from-llm 0.026 under its 0.30; 236 of 236 and the same farthest coin on 2026-10-13; §3.3), so the tint means exactly "the map could not honour this number". Under a what-if the same rule applies to the reader's own row, which is why the walkthrough's beat of §3.6 colours (0.049 refused) and the root case does not (0.001). A folded refined line tints under the same rule since 2026-09-12, its set the authored point and its value the composition of §3.5 (D38, amended 2026-09-12 by Felix's ruling on the display half of S21; what the folded number should be stays open).

Tension is the reader-facing payoff of the entire construction. On the flagship map, whose numbers are derived from the book authors' own confidence language by a rubric fixed before any number was assigned (D39), a tension badge is the book disagreeing with itself, and not the mapmaker disagreeing with the book.

4.4 The retired uniform reference (D36, 2026-07-16 to 2026-09-08)

From the ratification of D36 until D161 the deployed build solved against the uniform counting reference: entropy measured against the flat measure over live worlds, every joint cell at ½ (the joint-shaped completion of §3.1). Under it a line's rate had to be held by a mirror pair of conditional rows, P(E₀ | π) = P(E₀ | ¬π) = p, which made a strength-0 line inert and cancelled the arbitrary reference rate of the switch [proved] (CJ1/Prop C8, SOLVER_PROOFS §3.1; the CJ6 residual cancellation over the theory coordinate is machine-checked in lean/ArgmapProofs/Basic.lean). What remained after the mirror was a theorem: asserting a conditional lowered its antecedent by the drift tax, odds(π) = odds_ref(π) × P_ref(ψ|π)^p, the Judy Benjamin phenomenon arriving as an exact law [proved] (Thm C2, Adams restoration, SOLVER_PROOFS §6.2), so the free antecedent of one 0.8 line read 1/(1+2^0.8) = 0.3648. On the flagship that tax showed as the antecedent pull (SOLVER_SEMANTICS P8, closed by D161): a premise whose consequences are all confirmed FELL with each confirmation where Bayes raises it, 75 of 285 statements sat more than 0.01 from their directed values, and four of the five check badges past 0.10 were partly the tax. The single corpus weight was w = 400, chosen so the tax the ridge re-admitted stayed near 0.008 on the base case; the corpus-wide sweep over w in {100, 200, 400, 800, 1600} moved no statement past 0.10 and none across the 0.5 verdict line, the response monotone and saturating (the 800 to 1600 step at most 0.0041), so w = 400 already sat near the hard limit [measured, 2026-08-13] (truth_transport_probe.py --arm w).

All of it stays computable on the bench, and every one of its numbers is reproducible with one flag:

cd experiments/solver-prototypes
python3 solve_map.py <file.argmap> --reference d36 [ids...]

Under that flag the T2 toy reads its antecedent at 0.365 and the flagship @everyone-dies at 0.506 with 5 check badges past 0.10 (the flagship re-measured 2026-10-13, on the map with that day's grown line; under the shipped default 0.500, 0.624 and one, the headline's; on 2026-10-07, with $link-fine at 0.99 since 2026-10-06, 0.531 and 6 against 0.500, 0.609 and one; on 2026-09-28, the evening, with the undercut-kinds pass, D170, 0.534 and 6 against 0.500, 0.603 and one; on 2026-09-27, the evening, with the aligned-inverse batch, 0.540 and 6 against 0.500, 0.617 and one; that morning, on the map as restructured on 2026-09-25, 0.632 and 6 against 0.500, 0.708 and none). On 2026-09-11, after the 2026-09-08 evening content pass had closed two of the five this line used to count, the flag read 0.758 with 3 badges against the shipped 0.827 and none, and on 2026-09-23, under the one draw of §3.8, the shipped solve read 0.500, 0.796 and none. The closed-form anchor suite toy_run.py and the whole-corpus oracle jt_check.py pin that reference's values and are its record; the D36 oracle suites in solver-compile/tests name d36 explicitly. aref2, the directed reference of D159 with the D36 rows kept, is the second reading on the bench (--reference aref2).

How D36 and G meet [measured, 2026-09-23; the principle itself is proposed, not ratified]. The one-draw principle (ideas/plans/semantics-one-draw-release-2026-09-22.md, section 1 and the sections on the mirror and the convergence) reads every line's number as a share of the worlds its premise cuts out. Inside a cell (one joint assignment of the premises of a statement's lines) the lines that bite are one maximum-entropy draw of their in-force indicators, a for-line and an against-line never firing together; each rate is held in every cell; and only a sum past one is dead. Read against it, D36 had the half inside the cell and G has the half across cells:

1. D36's maximum entropy over the worlds, with the zero-sets and the rows, is the one draw on a single premise: a 0.6 support against a 0.3 objection reads the conclusion given the premise at 0.648 under D36 and 0.650 drawn. G multiplies independent coins except at one plus one: two 0.5 supports against a 0.2 objection read 0.807 under G, 0.744 drawn, 0.730 under D36.
2. D36 missed three things. Its entropy counted worlds, so the conclusion's free values where no line bites, and the combinations the exclusion removes, read as a premise's size: that is the drift tax above, and a 0.5 support against a 0.5 objection, which fit exactly, drew their open premise to 0.211 where G and the principle leave 0.500. The mirror held a rate on two cells, π and ¬π, so maximum entropy leaned the share into the sub-cells other premises cut: a 0.6 support beside a 0.3 objection on a nearly identical premise read 0.913 on the thin cell the objection misses, against 0.800 drawn (SOLVER_SEMANTICS P7's thin-slab price). And past one it had no dead excess, only infeasible rows the penalty escaped by shrinking the slab.
3. D161 cured the first by replacing maximum entropy with independent coins under the network reference. That holds a rate in every cell, and it gave up the draw inside the cell.

So the mirror is the principle on a two-cell partition, and the two histories meet at one place: D36 with its entropy measured over the lines' shares, its rates held in every cell and only the excess deleted is the principle, and so is G with the draw inside the cell. What stays different is a ruled choice, not a miss: D36 held rates in the posterior, where G and the principle hold them in the prior with count rows (D158 to D161). The toys and the scripts that measure all three are in experiments/solver-prototypes/mirror-toys-2026-09-23/.

5. A worked example

The smallest interesting document is one implication with nothing else:

@a
@c
$imp 0.8 @c | @a

No credence on either statement; one reasoning step of strength 0.8. Under the shipped solve (the network reference, ridge, the line at the bare count of 16) solving gives:

(Reproduce: cd experiments/solver-prototypes && python3 solve_map.py ../../examples/toys/a10-t2.argmap a-free c-free, the toy's ::free block; measured 2026-09-08; in the app, the Semantics audit map audit-reference, group R1. The retired reference's reading of the same file is --reference d36: P(a) 0.365.)

Each of the numbers is a place where a plausible expectation is wrong.

P(c|a) = 0.9, not 0.8. The authored strength is a floor, not a point: it guarantees c in at least 80% of the worlds where the premise holds (Prop A4's Q(ψ∧φ) ≥ p·Q(φ)). It buys that by being in force in 80% of worlds, and wherever it is in force the zero-set forces c outright. In the other 20% the line says nothing, and the network fills that silence at ½. So 0.8 + 0.2 × 0.5 = 0.9, the F1 fill identity [proved] (SOLVER_PROOFS §6.8), and it is the single most common source of surprise when reading a solved map: achieved conditionals sit above authored strengths, by exactly the unclaimed residual times the fill.

P(a) = 0.5, and it stays 0.5 whatever the rule says. The antecedent was never authored, and under the network reference asserting a rule about it does not move it: the toy's ::pinned block (the same line with @a 0.5 authored) reads the same 0.500 [measured] (same command; V6, Adams restoration, is the identity here rather than a repair). Under the retired reference the same document taxed a to 0.3648 (§4.4), and §7's row 1 records that the network reference, D159's directed reference and a Dirichlet completion all agree on 0.5000.

The sign of consilience is Bayesian. Give the same ground k consequents, each a 0.8 line and each pinned 0.9 (examples/toys/f-consilience.argmap; in the app, the Semantics audit map audit-forks, group F1): the ground reads 0.593 / 0.667 / 0.724 / 0.767 at k = 1 to 4, rising with each confirmed consequence, where the retired reference read 0.464 / 0.432 / 0.402 / 0.375, falling [measured] (solve_map.py at the default and at --reference d36, 2026-09-08). Refutation (f-refutation, the consequents pinned 0.2) falls under both: 0.225 / 0.134 / 0.081 shipped, 0.146 / 0.059 / 0.025 retired. Abduction (a7-abd-pin: a 0.99 rule, the consequent pinned 0.9) reads the ground at 0.600 against 0.450 retired. The plainest reason the reference changed is that first row.

6. Computing it

Naively the joint is exponential in the number of statements. In practice it is not, for a structural reason:

• The dual objective and its exact gradient are computable in O(n_cliques · 2^(w+1)) per iteration by junction-tree calibration, where w is the induced width of the moralized constraint graph [standard].
• Argument maps are narrow. If deleting c "escaping" cross-references leaves scopes admitting a join tree, then w ≤ (a+1) + c for premise arity a [proved] (Prop E2′, §9.2). Whether real corpora have that shape with small c is an empirical claim, and on this project's corpus the measured induced width runs 2 to 3 on the toys solved for §5 (2026-09-08), 2 to 6 on the small corpus files under the retired reference (2026-08-11) and 18 on the flagship under the shipped compile (15 under the retired reference, 16 under aref2; pinned in solver-compile/tests/reference-timing.test.ts, re-read 2026-09-27 on the map as restructured on 2026-09-25; 20, 14 and 19 on 2026-09-08, after the composition observable joined moralization) [measured]. What matters is the scaling: width 18 on a thousand-variable map is a largest clique of 2^18 cells rather than 2^1000.
• Ridge-Newton coordinate updates need only clique-local quantities, so one update touches O(diameter) messages [proved] (E4). This is what makes interactive re-solving feasible.

The route is the one the maximum-entropy expert-system shell SPIRIT took for conditional knowledge bases (Rödder, Reucher, Kulmann 2006: a junction tree of variable clusters representing the global distribution as a product of marginals), applied here to the penalised projection. Loopy belief propagation as an alternative was built into the kernel and measured under the shipped reference on 2026-09-09 and rejected for both the whole solve and a drag tier: its fixed point is five points off on if-built, is not unique on two corpus maps, and returns a different answer after a drag out and back (SOLVER_SCALING-2026-07-16.md §8).

The shipped implementation is a Rust junction-tree kernel compiled to WASM, running in the reader's browser. There is no server, and it works offline. On the keyed flagship under the shipped compile, measured 2026-09-08 on an idle desktop after the campaign's kernel pass (MVP_IMPL_NOTES 2026-09-08, lane W3-C; each timing run alone) [measured]: the compile 759 ms in node, the cold solve 942 ms (14 iterations), and a reader's what-if, the retarget of @everyone-dies to 0, 787 ms; in Chrome 1848 ms cold and 765 ms for the retarget, and 3995 ms / 805 ms with the CPU throttled fourfold, which is not a phone: a real device stays the measurement before a deploy. The retired reference solves the same map in about a tenth of that (cold 102 ms natively), because its tree is narrower; aref2 in about three times it. The document is block-partitioned, so editing one topic re-solves that topic at its own standalone cost rather than the whole document's.

The one draw inside the tree (D166, 2026-09-23). The draw of §3.8 depends, in each cell, on which lines bite there, so its table spans a block's premises and in-force indicators. Up to 16 variables the compile writes that table directly. The flagship's widest blocks are far past it (@shutdown has 26 lines for and 22 against on 2026-10-07, 27 for on 2026-09-23), and for them the compile builds a chain: per side the lines sorted by rate, a small state after each line holding the strongest level in force so far, a pair of region variables drawn from the two sides' final states, and each coin a conditional on the state before it and on its side's region, so the width of each link stays fixed however many lines the block has. The construction is exact wherever the draw is the nested layout (§7). Its cost has a particular shape: most of the cells it adds can hold no probability at all, because a deterministic table elsewhere in the tree kills them. On the flagship the tree grew from 0.47 million to 7.77 million cells and a reader's what-if from 158 ms to 3.0 s in node, and only 20.9 percent of those cells were live (its widest cliques 1 to 4 percent). The kernel now computes each clique's structural support when the map loads, the cells no deterministic table can reach, and runs its sweeps, readouts and incremental messages over those live cells only; every result is bit-identical to the dense loops. Together with three compile-side reductions (the readouts the chain left unread rewritten and their cascades dropped, the small blocks' tables factored through their in-force bits, a tie order for lines of equal rate) and a 40-minute elimination-order search, the flagship's what-if under the one draw takes 271 ms in node, against a bar of twice the pre-D166 what-if (about 340 ms) and 2,951 ms before [measured] (ideas/plans/kernel-onedraw-performance-2026-09-23.md section 8, medians of three, 2026-09-23). The pre-D166 model gains as well, 157 to 99 ms on the same kernel. Since the flip (2026-09-23) the shipped what-if on a desktop production build answers in 0.23 s from the press to the new numbers [measured, 2026-09-24, five visits, load 4.5], against 0.77 s before D166; on a phone-class CPU the estimate is about a second (the kit's flip-measure.md section 4, which also says why a browser cannot throttle the kernel's worker). What remains owed is the measurement that counts, a real phone. A what-if on a line's STRENGTH is different: it can re-sort the line's side of the chain, which is a new model the searched order was not found for. Since 2026-09-24 the compile maps the searched order onto that model (by variable name, or by the line each chain variable belongs to) and keeps it unless this model's own min-fill tree is cheaper; any elimination order gives the same answer, so only the price moves. On the flagship 192 of the 448 line moves re-sort a side: 172 of them now take a median of 172 ms in node against 505 ms on the min-fill tree they used to fall to [measured] (experiments/solver-prototypes/onedraw-perf-2026-09-23/transplant.md). For the other 20, where the mapped order grows too wide or too large, the compile since the same day prices the candidate trees by what the kernel pays for them (the cells no deterministic table kills, and the memory), and repairs a mapped order that grows too wide by re-running the greedy elimination on its tail. 19 of the 20 now avoid min-fill, and the 25 line moves that reach this check take 361 to 398 ms median against 555 to 570 before (the 20 alone, 437 to 456 against 592 to 632), within a memory budget of 256 MiB that every tree it takes meets at 64 to 227 MB [measured] (experiments/solver-prototypes/onedraw-perf-2026-09-23/guard.md).

Correctness is pinned three ways, all reproducible [measured]: a parity gate between the TypeScript compile solved in the WASM kernel and the python junction-tree oracle on 162 maps under the shipped reference and 167 under aref2 (the toys, the confusions, the skeptic set; on disk 2026-09-08 in experiments/solver-prototypes/fixtures/g/), worst 1.2e-7 on the shipped reference and one stiff aref2 map at 2e-6 against a 1e-6 gate (solver-compile/tests/g-parity.test.ts, MVP_IMPL_NOTES 2026-09-08); the flagship's acceptance numbers through the compile and the kernel agreeing with the python route (g-flagship.test.ts, root-whatif.test.ts, walkthrough.test.ts; this page's §3.6 numbers were read from both on 2026-09-08); and, for the retired reference, the older triple re-run 2026-08-11 (an explicit-joint oracle over 23 corpus files, worst marginal difference 4.42e-08, jt_check.py; 47 closed-form anchor cases carrying 54 assertions, toy_run.py; the TypeScript-to-oracle differential, worst 1.7e-7 on the comprehensive maps, differential.test.ts).

7. What is proved, what is measured, what is open

The property view of this ledger, one entry per invariance a reader may rely on with its layer, status, tolerance and battery, is SOLVER_INVARIANTS.md (opened 2026-08-28, stable Vn ids; the measured re-encoding equalities are bound to the tree by mvp/packages/solver-compile/tests/invariants.test.ts).

Why an I-projection in the first place has a literature answer the register cites entry by entry (2026-08-31): Paris (1994, with Vencovská) characterises minimum cross-entropy as the unique inference process satisfying a short list of common-sense principles (equivalence, irrelevant information, obstinacy, renaming, continuity, open-mindedness, ...), and the conditional-logic community holds its inference relations to probabilistic System P and to syntax splitting ((Rel) and (Ind), Kern-Isberner, Beierle, Brewka 2020) and to the kinematics principles descended from Jeffrey ((CaseRel), (CaseIrr); Hahn et al. 2025). V2, V6, V13, V18, V22, V24, V26 and V28 carry those names in parentheses. The network reference satisfies (Rel) and (Ind) exactly and declines (CInd) at colliders by design (§3.7). The two prior-art spokes of 2026-08-31 (ideas/plans/semantics-prior-art-*.md) are the source.

Hard-solve characterisation [proved elsewhere] (read 2026-08-31, ideas/plans/semantics-prior-art-2026-08-31/READS-2026-08-31.md): with one switch atom E per strengthed line and the prior m ⊗ Bern(r), the hard solve is the minimum cross-entropy adjustment to a conditional set per line, so Kern-Isberner (1998) Theorem 11 (the product form), Corollary 12, Theorem 29 and Theorem 31 (the unique adaptation obeying conditional preservation, the functional concept, logical consistency and representation invariance) apply to it verbatim. That reading was made of the D36 solve; under D161 the prior is the network and the targets are its Jeffrey updates, which is the same theorem family with R in place of the counting measure. Hard limit and hard-feasible maps only (the ridge breaks the paper's Corollary 32 by construction).

The full proof ledger is SOLVER_PROOFS-2026-07-16.md §13: 42 rows covering 43 result IDs (CJ1 and C8 are the same result; counts checked 2026-08-11), each with its own verdict, written for the D36 compile. What each cluster says under D161:

The one-draw rule (D166, 2026-09-23): what is proved and what is measured about it.

1. The rule D166 replaces is evidence weighing, exactly [proved]. In one cell of the network, with the conclusion C filled at ½ where no line forces it, write S̄ for the product of the supports' misses and T̄ for the objections'. Independent coins with the worlds where both sides fire deleted leave C true with mass (1 − S̄)T̄ + ½S̄T̄ and false with mass (1 − T̄)S̄ + ½S̄T̄, so the odds on C are [(2 − S̄)/S̄] · [T̄/(2 − T̄)]. Read alone, each side gives C at (1 + S)/2 or at (1 − T)/2, with S = 1 − S̄ and T = 1 − T̄; the odds above are those two likelihood ratios multiplied against even prior odds. So the pre-D166 cell rule is noisy-OR within each side and independent evidence across sides: one support at 0.85 against one objection at 0.15 reads 0.901, five supports at 0.9 against it read 1.000. (The algebra is the whole proof; the one-draw spoke, ideas/plans/semantics-one-draw-release-2026-09-22.md section 14, checks it numerically on five cases.)
2. Where the rates fit, the draw is two numbers per cell [proved]. Where both sides bite and the strongest rates sum below one, the maximum-entropy joint of the biting lines under the exclusion, each held at its rate, is an exponential family on the allowed states (the subsets of supports and the subsets of objections, sharing the empty state). It is therefore independent coins conditioned on the exclusion: inside the states where no objection fires, whose mass u includes the empty state, the supports fire independently at s_i / u, and the objections at t_j / v inside theirs. The two scalars solve z₀ = u ∏(1 − s_i/u) = v ∏(1 − t_j/v) and u + v − z₀ = 1, which has exactly one root (the argument and the exact bisection are in mvp/packages/solver-compile/src/cell-draw.ts, maxentDraw). With one line a side the rates alone decide it: s, t and 1 − s − t.
3. The chain is exact wherever the draw is the nested layout [proved]. In a cell where one side is silent the draw is the product of the coins; where both sides bite and their strongest biting rates sum to one or more it is the nested layout, which depends only on which line is strongest in force on each side. The chain of §6 visits each side's lines in decreasing rate, so the first line in force it meets is that side's strongest; the region pair carries the layout's four masses from the two strongest rates; and each coin's conditional (its own rate when out of force or when the other side is silent, its region when it is the strongest, its rate over the strongest's inside the region when weaker) multiplies out to the layout's table. The factorisation is an identity, so the solve is the same distribution. That argument is the proof: short, checkable by hand, not machine-checked. Floating point agrees [measured]: 1.1e-12 against the dense table on a toy where every collision reaches one, 5e-8 on the debate map and 1.1e-8 on he-xrisk (g_prior_probe.py --cell-draw chain-all), and the compile holds the python chain at 1e-6 on 82 fixtures, worst 1.5e-7, the flagship 5.5e-8 (2026-09-23).
4. Where the rates fit and a side has two lines or more, the chain approximates [measured]. There it uses the nested layout in place of the maximum-entropy draw of entry 2. Re-simulated on the flagship's wide blocks, the difference is at most 0.0010 per block (@asi-soon 0.0010, @inner-gap 0.0008, @eng-hard 0.0003, the rest 0; draw_sample.py --resim --fit-nested, 2026-09-23), against the release's gate of 0.005. Such cells carry 17.6 percent of @asi-soon's worlds, 1.6 of @inner-gap's, 1.2 of @eng-hard's and none of the other wide blocks'. On a toy built to be all fit cells with two lines a side the gap is 0.016 (0.706 against 0.722), the largest found.

Measured under the shipped solve, the rows a reader can hold the project to (each re-run on the date given, through the compile and the kernel unless a script is named; rows 1 to 11 were taken under D161, and re-measured under D166 on 2026-09-23 rows 1, 2 and 7 read the same, since their toys carry no opposed lines and every draw there is the product, row 3 moves where noted, and row 12 is D166's own):

1. The free antecedent of one implication reads 0.5000 exactly, under the network reference, aref2 and a Dirichlet completion alike; the mirror pair and the fan read 0.5000 too (PLACEMENT_PROBE 15; §5 re-run 2026-09-08 with solve_map.py: 0.500).
2. Consilience has the Bayesian sign: 0.593 / 0.667 / 0.724 / 0.767 at k = 1 to 4 confirmed consequents where the retired reference read 0.464 down to 0.375; refutation falls under every reference; abduction reads 0.600 against 0.450 retired (§5, 2026-09-08).
3. Cancellation: equal support and opposition from one premise at p ≤ ½ cancel exactly to the empty map (f-cancel-pair: the p = 0.3 and p = 0.5 members read 0.500 on both statements, 2026-09-08); above ½ the two sides cannot both be coins of one three-state pair and the premise reads 0.192 at p = 0.8, the shape S20's family covers. Under D166 it reads 0.215, the dead mass being the excess 0.6 where the independent coins deleted their product 0.64 (2026-09-23).
4. The flagship: @everyone-dies 0.827 (0.758 retired, 0.818 under aref2 with the same counts; all three solve_map.py 2026-09-08), its check 0.88..0.98; on the map as it then stood badges past 0.10 went 5 to 1, the four the uniform reference alone created clearing with the map text unchanged (@steering-finds-subversion, @goals, @corrig-antinatural, @everyone-dies) and @evo-analogy at 0.417 against 0.75..0.95 left standing as the book's own under every reference (D161 item 7; solve_map.py 2026-09-08 agreeing on the headline and the badge count). The 2026-09-08 evening content pass then closed that one too, by mapping the chapter's own case for the analogy rather than by moving a number: re-measured 2026-09-11, the shipped solve badges nothing past 0.10 (widest gap @everyone-dies, 0.053) and the retired reference badges 3 (@steering-finds-subversion 0.624, @goals 0.708, @everyone-dies 0.758, all against checks whose floor is 0.85 or above).
5. The visible map holds no root: with each of the 224 pinned statements' own row removed, the rest of the map holds it at about one flip (PLACEMENT_PROBE 22, a probe, 2026-09-07). The counts therefore come from width and kind only, and a badge on the flagship is the authors' assertions disagreeing with each other through the authors' own steps.
6. The kind table's acceptance tests at the ruled tier (D161 appendix item 11; g-flagship.test.ts, socrates-tier.test.ts, 2026-09-08): (a) the flagship's badges as authored do not change, one statement moving past 0.05 (@nat-abs 0.140 to 0.191); (b) formal holds 0.990 on the Socrates copies and deductive at 1000 reads 0.930, the 0.02 miss on the record; (c) under the P6 set the retreat lands on analogy and testimony before mechanism and never on deductive (§3.6); (d) the parallel-leaf ladder's return at the K3 default, 0.10 across four leaves, a stated price (S19); (e) he-xrisk's three incident lines meet the author's check 0.85 within the badge threshold at the K3 floor (0.837) and miss it at one flip each (0.750).
7. The what-if on a true root and on a derived lemma (§3.6): @llm-nice 0.1 read 0.101 with nothing bent; @asi-soon 0.1 read 0.124, tinted (2026-09-08).
8. The 224 pairs all inside their intervals under the shipped compile, and nothing on the map outside its authored set (§3.3, §4.3, 2026-09-08); under D166 the 239 pins of the map as it then stood all sit within 0.01 of their sets (2026-09-23), and the 237 of the map as restructured on 2026-09-25 all inside their intervals (2026-09-27, and again 2026-10-07), as are the 236 of the map with the grown line (2026-10-13).
9. The engines agree: 162 maps under the shipped reference to 1.2e-7 and 167 under aref2 with one stiff map at 2e-6 (§6, on disk 2026-09-08).
10. Kind agreement: 251 of 348 lines, kappa 0.651 on the seven kinds (D161 appendix item 10, recomputed 2026-09-08 from the two passes' files).
11. The flagship's pins under the width rule: median 18 flips, minimum 0.5, maximum 38, 55 of 224 below 16, 3 below 4 (recounted 2026-09-08 from argmap-query pinned-roots, §3.3; 56 of 237 and 4 on 2026-10-07, 56 of 236 and 4 on 2026-10-13). As authored, the Walley weights move 53 statements past 0.01 against the old tier and none past 0.05 (max 0.036, @c13-monitor), D161 item 7.
12. The one draw (D166; 2026-09-23 through the compile and the kernel, the python oracle agreeing to 5.5e-8): on the flagship 19 statements move past 0.01 and none past 0.05, sixteen down and three up; @shutdown 0.999 to 0.957, the headline @everyone-dies 0.827 to 0.796. Of the 64 checked statements, 15 sit outside their range by more than 0.01 against 19 before; still no badge past 0.10, the widest gap the headline's, 0.084 short of 0.88 (0.053 before). The debate map's headline reads 0.230 against 0.182 before, and he-xrisk moves three statements by 0.011 to 0.022.

Retired, each with a tombstone a later reader can reopen from (D161 item 8):

• the uniform counting reference with its drift tax and antecedent pull: §4.4 above is the tombstone, --reference d36 the bench; SOLVER_SEMANTICS P8 is CLOSED (2026-09-08) and its items 1 to 4 stay as the record of the retired solve, the anchor family, the flagship inventory (75 of 285 statements more than 0.01 from their directed values, four of five badges partly the tax);
• the structural term of the graded-law reading, P(a) = 1 / (1 + 2^D), exact for the uniform reference (T2 0.3648; the fan 0.2481, 0.0588, 0.0039 at k = 2, 5, 10): retired by the consilience sign (row 2) and by the four badges (row 4), kept in the toy battery's D36 column;
• the counting cut (1/4) and per-parent normalization (½) of the dead cell, against G's 1/3 (two hard rules that cannot both fire): at full strength every network candidate reads 1/3 by conditioning the roots on the contradiction, and at soft strength G reads the contradiction as evidence against the joint premises (fork 8);
• the interval reading of pairs (§3.3);
• the Kish count for pooled positions (D160): a panelist raising their credence near unanimity lowered the pooled claim, structural to any count that decreases in dispersion; P10 stays parked, a pool enters as one row at the head-weighted mean, and no shipped map pools.

Refuted earlier and still standing, restated:

1. Documents are not generative models under the uniform reference (Conj C3, refuted 2026-07-16): a map with fully authored conditionals solved at maximum entropy against the counting measure is not in general its Bayesian network (a v-structure counterexample places covariance +0.045 between parents where the BN puts zero); the forest case (in-degree ≤ 1) is the proved sufficient direction (Thm C3′). Under D161 the question changes shape: the prior IS the network by construction and the targets are Jeffrey updates of it, so what the refutation now says is why the reference had to be the network rather than the counting measure. What it does not say is that the solved map is a Bayesian network: a target on a derived statement is a soft claim the network never made, and the I-projection of a BN onto such a claim is not a BN in the same graph.
2. Undercut strength-monotonicity failed under the pre-2026-07 asymmetric compile: a non-monotone bump traceable to the undercut's own bookkeeping drift. The ratified compile dissolves it (proved for the flat form), but the refutation is why the general-graph claim is still marked open rather than assumed.

Named open problems (this document's editorial order; each Sn is stated in SOLVER_SEMANTICS with a lint note on the authored shape, so an author who writes the shape learns the reading is open):

• S18, premise-less lines (fork 2, with forks 1 and 11): decided by D166 (R2, 2026-09-23) as the mechanism reading: a floor is a line whose premise is every world, it stacks with its neighbours where nothing objects and joins the one draw where something does. It is applied after the release; until then the solve keeps the placeholder, targets that pool, and lint I4 names it. The application owes three answers: how a voice is written (a band from the rubric's pair column, effectively settled), whether agreeing voices count (a headcount ruling) and how firmly a stated credence is held (a firmness ruling, the one that moves numbers: on the debate map 30 statements past 0.01 with voices as rubric bands, against 7 with the placeholder).
• S19, parallel lines from one premise into one conclusion (fork 7): closed by D166. They are same-side shares of one draw, independent where no objection bites, which is what the placeholder already did, so no number moves. The ladder's return under counts stays the stated price: 0.2696 at one leaf to 0.1690 at four at the K3 default (0.10 across the ladder; flat at 0.1122 without counts), unchanged under D166 (2026-09-23). No shipped map carries the shape. Lint I5.
• S20, two coinciding pairs from different premises into one statement (fork 12, fork 6 behind it): closed by D166. The placeholder had them vote by product (0.9 and 0.7 give 0.955 in the cell where both bite), Bayes under the two arguments' independence given the conclusion; under the one draw the four lines share the cell, the strongest for-share 0.9 against the strongest against-share 0.3, and the cell reads 0.875 (fixture e29's @vote 0.883 to 0.839 through the network, 2026-09-23). The shipped floor register does not carry the shape. Fork 6, which waited behind this reading, stays open.
• S21, the refined line's own number (fork 3, reopened): a block-local definition is wanted; the composition ships meanwhile, tinted against the authored point since 2026-09-12 (§4.3), with its interior-fill error on deep spines (§3.5).
• The width of an unpinned claim's value (the interval instrument): what a reader sees on a claim nobody priced was a point and, beside it, the # check: interval the format carries (the toy n-not-a-number, 2026-09-18, called the interval instrument open under G: the bench's sublevel interval reads a placeholder unit on floor rows). Since 2026-09-25 the editor draws the unpriced share (GLOSSARY; editor/src/unpriced-share.ts): the mass where no strengthed line into the claim has its premises hold (the premise side; the coin's miss inside the premise mass is the author's rate, not fill), which the network reference fills in at the fill rate f = P(claim | no line's premises hold): ½ for a leaf (§3.1), and ½ unless the rest of the map moves it in general (downstream clashes and the pairs on the downstream lines' other premises move it; [measured] 2026-09-27 on the flagship at rest, 6 of 67 claims depart by more than 0.01, the largest 0.795 on @risk-unbounded at a width of 0.015%, and under question 25's what-if (@misaligned-when-built at 0) the pin moves 24 of the 51 drawn bands' rates by more than 0.01 and 17 of them below 0.4, @align-hard to 0.00004); the band's sentence prints the rate where it does not read 0.50. Its WIDTH is exact for a claim with one line, 1 minus the line's premise mass [measured] (the flagship's @if-built on 2026-09-25, before that day's restructure gave it six lines: at rest 0.155 around 0.880; at the demo premise's 1%: 0.99 around 0.506; at 0: 1, the silent claim). For several lines (2026-09-27; the lines counted are the forcing ones, never an undercut's or a refined summary's) it is exact where the lines' premise events partition or nest, 1 minus the summed masses of the outermost lines [proved] (a truth table over the premise expressions; [measured] the flagship's @everyone-dies at 0.184 on the map of that morning and @if-built at 0.018, equal to the probe experiments/solver-prototypes/unpriced_exact_probe.py on the solved joint), and otherwise an upper BOUND, 1 minus the summed masses of lines whose premises exclude one another, which the sentence names with "up to" (loose on the flagship: 39 claims, most by more than 5 points; 40 since the aligned-inverse batch of the same evening, D168, whose four lines into the title claim overlap, so the bound reads "up to 13%" there where the exact width is 0). Since 2026-09-27 the width and the rate are exact wherever a solve has landed [measured]: the kernel's evidence entry reads w = Z_E / Z and f off the calibration the solve left, E the conjunction of each forcing line's NOT(premise) table in the clique that already holds it (no widening), equal to the python oracle (dump_unpriced_fixtures.py) within 1e-6 on every shipped map, the flagship at rest and under question 25 (the title claim 0.8329543 at 0.4267 on the map of that morning; exactly 0 at 0.0445 since the aligned-inverse batch of the same evening, D168, and 0 at rest too: its two inverse lines price every world the reference had filled); the shipped solved sidecar carries the same numbers for the first paint, and only a frame before an exact landing (a drag) still shows the slab bound, as an upper limit that lasts until the solve lands. It is the plain bound: a cap at min(bound, 2v, 2(1 − v)) assumed f = ½, fell below the exact width where f is far from it (question 25's @align-hard: f 0.00004, w 0.419 against 2v = 0.215), and was retired on 2026-09-27. Its PLACEMENT is the band clamp(v − w·f) to clamp(v + w·(1 − f)), the value with the fill at 0 and at 1 [proved] (v = (1 − w)·q + w·f, q what the lines deliver where some premise holds), with f the solve's own rate wherever it supplies one and ½ elsewhere, which is exact for a leaf with one line and an approximation otherwise (a claim with consumers is pulled off ½ where its premises fail, the G0 grounded reading). The gauge draws lo..v, the fill's paler top (Felix's R1, 2026-09-25); the upper bound is the sentence's. It is a decomposition of the solved point, not a credal interval: the objective's sublevel interval (§4.2's ridge band, the bench probe) stays open as a reader instrument, and the two answer different questions.
• The constants: the per-kind counts, s = 2, the 0.01 point cap and the 0.01 tint tolerance, and K1b's 0.02 miss on the two-premise Socrates copy: convention until a map's acceptance tests move them, and a ruling owed on the miss.
• The contradiction's display (fork 8's remainder): with the roots pinned, two rules that cannot both fire hide their conflict in root anti-correlation, which no marginal shows. D166 item 6 agrees the answer, a collision audit listing each case with a dead excess and how often that case occurs; it is not built.
• The objection lines' numbers: on the flagship most are role defaults (0.15 or 0.20) where the book gives no rate, and under D166 each is a cap in the cases where its objection stands unanswered. D166 has them documented as defaults, which the rubric page does in its section 2.4, until a re-elicitation pass asks the book the question a cap needs (written down in the one-draw spoke, section 15); none has run.
• Declared independence among same-side lines (D166, R1): deferred as a format question. Until the format has it, two lines over one premise are two mechanisms (D160 item 2), so the same reason written twice counts twice, and argmap-query restate-audit is the author's check.
• The kernel timing without a phone gate: the desktop numbers of §6, and the one draw's what-if at 271 ms in node (2026-09-23); a real device stays the measurement before a deploy.
• Switch-switch independence is unpriced (P2) and the solver uses the freedom: on the flagship under the retired reference the response to an objection fired with probability 0.91 to 0.98 given the objection fired, against authored rates of 0.75 to 0.90 (a pairwise-mirror probe, SOLVER_PAIRWISE_MIRROR-2026-08-22.md, nothing ratified); its measured face under conflict was P9, k parallel leaves giving way more than one line (0.524 / 0.502 / 0.376 / 0.237 at k = 1/2/4/8 under D36), ruled a stated limit (D158: refinement replaces, V8, is the contract), closed for the no-conflict case under G and reopened as S19's price. D166 prices one face of it: inside a cell where a support and an objection bite, the exclusion holds and independence is what gives. Across cells, and within a side that nothing opposes, it stays unpriced.
• Carried over unchanged: CJ9 (the accumulation-ordering inequality; FKG-type arguments fail because the zero-set-masked Gibbs measure is not log-supermodular), CJ10 / D1 general (undercut monotonicity on general graphs), C5c / CJ12 (the general floor algebra for mixed premise contexts), B2 bare / CJ11 (well-posedness of the unweighted KL penalty), D2 (reinstatement fixed points on undercut chains), S5 cycles, S8 arity, S12 credal links, S13 mixed statement kinds.

What is no longer open, though earlier editions of this page listed it: the balancing prior (§3.3: the interior point is the network's own fill restricted to the interval); the antecedent pull (retired with its reference, P8); the thin-slab price (P7, closed under G, §4.2); the undercut channel split (settled by D36's factored-A compile, §3.4, as the previous edition already said).

Double counting across a junction: one measured detector, no proof (2026-08-22, under the retired reference) [measured]. Two premises of one line that share a consideration co-move, and the solve prices that when the consideration is a statement: on toy T8 (examples/toys/t8-shared-cause.argmap, against t8b-separate-causes) the shared root raises the AND consumer and lowers the OR consumer against the same lines with separate roots. On the comprehensive EN map one junction of 87 cleared the detector's floor ($wst-race, which conjoins a statement with a statement derived from it). The detector is blind wherever a premise is pinned (72 of the 87 junctions), which is the residual rule's own case and a lint's job, not a solver readout. Memo experiments/solver-prototypes/SOLVER_COVARIANCE-2026-08-22.md; not re-run under the network reference.

8. Limitations

Listed here, because a reader who finds these on their own will trust everything else less:

• Statements are binary. No categorical or continuous variables.
• The reference measure is a choice, and the choice is the map's own network with uniform fill-ins (D159, D161). It is directed: writing ~a | ~c instead of c | a is a different network: on §5's document written contrapositively the antecedent a reads 0.300 instead of 0.500 [measured] (solve_map.py at the default on a two-statement toy, 2026-09-08; V15 says exactly this: the given bar stays directional and contraposition is not a rewrite), which is the price of a directed semantics, carried by the authoring tutorial's translation rule. The uniform counting measure was the earlier choice, and §4.4 says what it cost.
• The numbers are only as good as the rubric that produced them. On the flagship map they derive from the source authors' own confidence language by a pre-registered rubric: the table, the protocol that applied it and the badge methodology are published as rubric.html (since 2026-09-11), with the short version on the app's "How ArgMap works" page; the dated registration entries stay in the repository's authoring log (not yet public, like the rest of the repository; the newer maps embed their rubric in the map file itself). That makes tensions auditable. But a verbal-to-probability rubric is itself a modeling decision, and a different rubric would move most of them.
• The counts are a rubric on top of a rubric. The D39 rubric turns the authors' confidence language into values; the kind rubric turns their reasoning language into counts. One line in four got its kind by a judgment call (kappa 0.651 on the kinds), and the per-kind constants are convention. What the acceptance tests show is that the book as authored is nearly indifferent to the table (one statement past 0.05); what the table decides is the reader's what-if, and there the flagship's own pins, at median 18 flips, give before its mechanisms at 64.
• The visible flagship holds no root (§7 row 5): the book's numbers are almost entirely the authors' assertions, and the solve fills in between them. A badge on the flagship is therefore the authors' assertions disagreeing with each other through the authors' own steps, and nothing the structure imposes.
• Explaining away is a feature, and (CInd) is not a property the map claims (§3.7).
• The narrowness result is empirical on one corpus. Width 18 on the flagship is real evidence, and it is not a theorem about argument maps in general. A map with many cross-references between refinement groups would be wider, and nothing prevents one. Note also that the constant moves with the compile and the map: it was 7 before the 2026-07 factored-undercut compile, 11 under D36 for most of that reference's life, 14 under it on 2026-09-08 and 15 on today's map, and 20 under the network reference on 2026-09-08, whose reference factors and composition observables join moralization, 18 on today's map (2026-09-27, §6). The bound (Prop E2′) is what is proved.
• This is not a truth oracle. The solve says what a set of authored numbers jointly implies. It has no view on whether they are right.

9. Where to go deeper

Reading order, by what you want:

The ratified model, compactly: SOLVER_SEMANTICS.md. The authoritative statement of D36 as amended by D161: the compile, the objective, the display rules, the known problems (Pn) and open questions (Sn, S18 to S21 the current ones). Start here for anything normative. The decision itself is DECISIONS D161 (2026-09-08), with D159 (the reference) and D160 (pools) before it.

Why it is built this way: SOLVER_FAQ-2026-07-14.md answers the eleven questions that recur: why penalize the projection at all, whether the method is standard, what the dual is, which optimizer runs where. Its answers were written for the uniform reference; the projection and the ridge carry over unchanged, the reference does not.

The derivations (all written for the D36 compile; §7's cluster table says what each still says under D161):

The proof ledger: SOLVER_CONJECTURES-2026-07-16.md states the obligations (CJn, append-only, now running to CJ12). SOLVER_PROOFS-2026-07-16.md discharges CJ1 to CJ8 (CJ9 to CJ12 are the open residue that proof pass itself surfaced) and carries the §13 status table that §7 above summarizes. §13 is the sole authority on verdicts: where any other document disagrees with it, it wins.

The semantics review that produced D161, read for provenance: ideas/plans/semantics-antecedent-pull-2026-09-06.md (the two verbs, the counts, the forks), ideas/plans/semantics-generative-proposal-2026-09-03.md (the G compile and its ledger), experiments/solver-prototypes/PLACEMENT_PROBE-2026-09-04.md (the probe record, sections 15 to 23), and the campaign that shipped it, ideas/plans/campaign-semantics-implementation-2026-09-08.md with its skeptic's and fit reviewer's reports.

Probe and session records, read for provenance rather than doctrine: SOLVER_UNDERCUT_PROBE-2026-07-16.md and SOLVER_SCALING-2026-07-16.md (probe records), SOLVER_REVIEW-2026-07-16.md (a review whose findings were folded in), and SOLVER_SESSION_NOTES-2026-07-12.md / SOLVER_SESSION_PREP-2026-07-11.md (historical: superseded by D36, and the latter's decision chain stops at D24). Every solver doc declares its kind: in its frontmatter (see GLOSSARY solver-doc kind), so this classification is checkable at the file rather than only here. This section names all 17 SOLVER_*.md docs at the repository root (ls SOLVER_*.md, 17 on 2026-09-08; SOLVER_INVARIANTS.md joined on 2026-08-28), and every doc it names exists; no test binds that list, so it was checked by hand on that date (find . -name 'SOLVER_*.md' also reports three probe records filed beside their scripts under experiments/solver-prototypes/: SOLVER_WIDENING-2026-08-22.md, SOLVER_PAIRWISE_MIRROR-2026-08-22.md, SOLVER_COVARIANCE-2026-08-22.md).

Machine-checked fragments: lean/. A Lean 4 pilot against Mathlib covering the CTT multiplicity count (CJ6), the structural layer of contraposition symmetry (CJ4), and the finite Gibbs variational principle that the slab lemma rests on. This is a pilot, not a formalized theory: one ledger row of 42 is fully machine-checked (about 2%; about 7% counting partials), and 39 rows have no Lean content at all. lean/README.md carries the row-by-row status and the roadmap. Do not read the pilot's existence as a claim about the ledger as a whole.

The paper: paper/ drafts the publishable treatment, and its outline and formal-claim inventory is PAPER_OUTLINE-2026-07-12.md (written for the uniform reference; its §7 open-problem list predates D36 and D161).

Run it yourself, once the repository is public: these commands run inside the repository; until it opens they are the record of how every number was produced, not something this page can hand you. experiments/solver-prototypes/ is the reference implementation. Every solver number in §§3 to 6 reproduces there or in the shipped stack: the toys and the flagship through solve_map.py (the default is the shipped reference since 2026-09-08; --reference d36 gives the retired one, and --override id=value is the reader's what-if), the kernel-side numbers through the oracle-gated tests in mvp/packages/solver-compile/tests (ORACLES=1 npm test), and the timings through the editor's proofs/reference-timing.mjs in a browser.

cd experiments/solver-prototypes
python3 solve_map.py <file.argmap> --top 10          # largest gaps and tensions, the shipped solve
python3 solve_map.py <file.argmap> --override id=0.1 # the reader's what-if, revision
python3 solve_map.py <file.argmap> --reference d36   # the retired uniform reference
python3 toy_run.py                                   # the retired reference's closed-form anchors
python3 jt_check.py                                  # the retired reference's whole-corpus oracle

Terminology: GLOSSARY.md is canonical for every term used above (given bar, network reference, count, kind, authored set, revision and conditioning, tension, solved value, in-force, drift tax and antecedent pull for the retired reference, ...).

This document is the keystone rung of a deliberate ladder (DECISIONS D61): the in-app "How this works" panel introduces the ideas without notation, the authoring tutorial gives the rules operationally, this document gives the model and the status, and the SOLVER_* docs, paper/ and lean/ carry the derivations, the publishable treatment and the machine-checked fragments. If you find a claim here that its cited source does not support, that is a bug. The citation is the contract, and it binds before the sources are public: every citation is exact so that opening the repository makes each one checkable by anyone.