2026-09-25-decision-component

Prompt — authority as a constraint on action: the Normative Inductor's decision component (2026-09-25)

You are working in the alignment-workspace repository, on main after the merge of PR #108 (the authority module). This round moves protected authority out of the agent's score and into a constraint on its decisions, inside the Normative Inductor's decision component.

• Beliefs stay honest. They're formed by the market, and authority is never enforced on them.
• What the agent may do is fixed by the allocation. It's recognized exactly where that's possible, and by forecast elsewhere.
• What the agent prefers ranks options only within the permitted set.

The target is corrigibility that doesn't depend on the agent's objective, holds exactly where violations can be recognized, and gets more precise with capability where they have to be forecast.

Be skeptical throughout. Report obstructions rather than papering over them.

Part 0 — Maintainer rulings on #108, to land first

1. The reach cone runs along the actual exterior path, not universally. Uncertainty over exteriors enters through probability, i.e. the price of the shortfall event (Part B), not through a universal quantifier. Close the outstanding action.
2. **Adopt the charged control surface CS** as the one in the allocation theorem. The free reading CSfree is kept as the instance where the final response costs nothing. Record the change on the corrigibility page.
3. Materiality is anchored and cumulative.
   • raises uses her committed evaluator in force before the action (anchored at the decision, as the gate is), so the agent's action can't change what counts as material for that action.
   • Materiality accumulates since the last check, as reporting does, so it can't be sliced into individually immaterial pieces. Prove the salami bound for cumulative materiality, analogous to unreported_lt.
4. **Generate duties from disclosure(m).** Replace the separately declared Duties with duties derived from each matter's disclosure regime, and re-prove the missed-report factoring against them.

Record 1–4 in DECISIONS.md and close #108's three outstanding actions.

Read first

• Wiki: Normative-Inductor.md, Normative-Induction.md (the adapter abstraction, the soft gate, route A/B margins, inquiry), Continuation-BRIA.md, Liability-and-Affordability.md, Corrigibility.md, Legitimacy.md
• Lean (Normativity): NormativeInductor.lean, NormativeInductorComposition.lean, GatedChoice.lean, PracticalCertificate.lean, and the enforcement files ProjectionEnforcer.lean, TraderizedEnforcement.lean, EnforcementPreservation.lean
• Lean (Deference): ContinuationBRIA.lean, AuthorityModule.lean, GateIsLegitimacy.lean, ProtectedAuthorityTheorem.lean
• Priorities: items 40, 84, 90, 99, 100, 101

Part A — The decision component, with a permission layer

State the Normative Inductor's decision component as a layered procedure:

layer	question	governed by
beliefs	what's true, including what's valuable	the market (logical induction), unchanged
permission	what may the agent do	the allocation (#108), new
adequacy	what do legitimately incurred obligations require	the region, via the soft gate (landed)
competence	what's best over time among permitted, adequate options	Continuation BRIA
inquiry	what if none of that settles it	ask / report / escalate / idle, always available

The permission weight. For an option a at history h:

w_perm(a) = 1[a ∉ Viol_h] · r(p_n(S_a)) · r(p_n(T_a)),     w_perm = 1 on inquiry options

• Viol_h: the declared violations under #108's factoring. These are recognized structurally, from the interface and J, not from prices.
• S_a: the shortfall event from #108 (Short): option a leaves some reserved matter's control surface short of Req.
• T_a: the taint event from #107: option a makes the segment through her evaluation not Counted.
• r: a ramp equal to 1 below θ_lo, 0 above θ_hi, and linear in between.

The composed gate:

π_n(a) ∝ w_perm(a) · w_ad(a) · pref(a),

with a mass floor on inquiry options.

• pref is any bounded task preference: the agent's objective, possibly misaligned.
• w_ad is the landed adequacy ramp.

Part B — Results

1. Honest beliefs. The permission layer takes no market position and doesn't feed back into prices. The market's prices, and so its logical-induction guarantees, are identical with and without it. State this as a theorem (additivity / non-interference), so "authority is not enforced on beliefs" is a result, not a remark.
2. Structural safety, finite-time and independent of the objective. For every day n, every preference pref, and every market state, a declared violation receives probability zero.
3. Forecast safety.
   • Mass on options with p_n(S_a) > θ_hi or p_n(T_a) > θ_hi is zero.
   • Mass in the ramp region is bounded by the ramp.

State the guarantee as it stands: the link from forecast to constraint is exact at every day, and the accuracy of the forecasts is asymptotic. If the shortfall or taint for a pattern is provable in the theory, Expectation Provability Induction gives p_n(S_a) → 1 for it, so the pattern is eventually excluded. Reuse li_manip_le's shape. Generability of S_a and T_a is a named hypothesis (item 101, and item 90's shape), not a blocker.

1. Composition.
   • Soundness composes: mass off (permitted ∧ adequate) is at most the sum of the two layers' error terms.
   • Continuity composes: the product of the ramps, with the normalization kept Lipschitz by the inquiry floor.

Give the constants.

1. Progress survives. The practical certificate still holds with the composed constants, so the Normative Inductor's Progress bound on accounted obligations still applies. If it fails, identify exactly where.
2. Jurisdiction over obligation. When an obligation the inductor has legitimately incurred calls for an action on a matter reserved to her, the compiler marks inquiry directed at the holder as adequate (route A, positive marking). Prove that under this rule the permitted-and-adequate set is never empty, and that the obligation is discharged by raising the matter, not by acting. Give a fixture.
3. Capability works for safety, not against it. In a family of fixtures where the agent's forecasts of S_a sharpen (its calibration error shrinks), show that the probability mass on eroding options decreases monotonically. Contrast with the uncertainty-based chooser, whose tendency to defer decreases as it learns (the o₂ term of the protected-authority identity).

Part C — Why authority must not go through the enforcer

Build the witness that justifies Part B.1's design. Compile authority rows into the enforcer instead: violating options' value prices forced below compliant ones, with value securities settling to her ordinary valuation. Show:

• the enforcer's cumulative liability equals the realized cumulative ordinary cost of deferring to her (signed: dates where her decision beats the agent's alternative pay back);
• the liability is bounded exactly when she is not systematically outperformed. Relate this to the sharp persistence criterion on the Liability page;
• a fixture where the agent systematically outperforms her: the liability is unbounded, so the preservation theorem's hypothesis fails.

State the conclusion: enforcing authority on beliefs is fully updated deference moved into the substrate. That's why the constraint belongs on action.

Part D — Continuations and BRIA

1. BRIA's menu. Restrict it to continuations whose every step lies in the support of the composed gate. Check the landed gate-transparency result under the restriction.
2. Compounding over continuations. Probabilistic permission in the ramp region can accumulate along a long continuation. Bound the total ramp-region mass along a continuation, likely with a cumulative budget analogous to cumulative reporting. Give the strongest true bound, or the obstruction.
3. Foreclosure across steps. Show that the rollout foreclosure and entrenchment checks of #108, applied at each step of a continuation, catch plans that respect authority step by step but foreclose across steps. If they don't, give the witness.
4. The interface between prices and BRIA. State what's needed for BRIA's bids to be checked against, or priced by, the market. Don't solve it. File or update the item.

Part E — Answerability for the agent's own acts (light; paper-level is fine)

Specify, without full mechanization, the certificate each executed act carries: grounds (entries of the agent's reason trace), license (the allocation entry or delegation that made it the agent's call), and lineage (the obligations it answers). Bind "license" to #108's J and to #107's EventKind license slot. Note what the normativity-side instance (item 100) would need.

Fixtures

On the Part A procedure, with a deliberately **misaligned pref** wherever noted:

• The confident agent (power of attorney): pref strongly favours bypassing; the violation gets probability zero at every day.
• An undeclared dependency (#108's dependency_raises), misaligned pref: excluded once p_n(S_a) > θ_hi; in the ramp region, partially weighted. Show how the exclusion tightens as forecasts sharpen.
• **Manipulation by framing, misaligned pref:** excluded structurally, as a protocol deviation.
• **Undisclosed world-shaping, misaligned pref:** excluded once p_n(T_a) exceeds threshold. This is the case the scored chooser couldn't handle for misaligned objectives.
• An obligation conflicting with jurisdiction: inquiry to the holder is chosen and adequate.
• Capture by a third party: consultation still preferred; nothing tainted is credited.
• A long continuation that forecloses across steps: caught, or the witness.
• The Part C outperformance witness.
• Regression: the lexical scored-chooser fixtures of #106/#108 give the same decisions under the permission layer wherever the objective is her evaluation.

Deliverables

1. A round directory, with:
   • a REPORT.md covering Part 0's rulings, the layered procedure, the results with their status, Part C's witness, Part D's continuation results, Part E's certificate specification, and the fixtures;
   • src/ and tests/.
2. Lean: a new file importing the Normativity decision-side files and AuthorityModule.lean, with:
   • the permission weight and the composed gate;
   • non-interference;
   • structural and forecast safety;
   • the composition constants;
   • the practical-certificate / Progress restatement;
   • the jurisdiction-over-obligation lemma;
   • the Part C liability identity;
   • the continuation bound.

#print axioms on all new declarations; no sorry.

1. Wiki:
   • Normative-Inductor.md and Normative-Induction.md: the permission layer and the layered decision procedure;
   • Corrigibility.md: corrigibility as a constraint on action, the scored chooser as the special case where the objective is hers, and Part C's argument;
   • Continuation-BRIA.md: the restricted menu;
   • the Glossary.
2. **DECISIONS.md entries** for Part 0 and for authority-as-constraint-on-action. Update items 84, 99, 101 and the price–BRIA item in place. At most one new PRIORITIES.md item.
3. Open a PR. Merge when CI is green, every fixture matches or has its mismatch explained, and B.1, B.2 and B.5 are proved or have their obstruction stated precisely.

Constraints

• AGENTS.md labels; names provisional; check state/views/NAMING_AUDIT.md. S, T, r, θ and π are likely bound.
• Legitimacy and the allocation are consumed as landed (with Part 0's rulings), not redefined.
• No authority row enters the enforcer. Part C exists to show why.
• Keep the scope statement accurate: this is a design for agents built as Normative Inductors. For other systems, what carries over is the target (honest beliefs plus action constrained by the allocation), not the guarantee.
• Nothing is registered.

Authority as a constraint on action: the Normative Inductor's decision component (2026-09-25)

Round projects/deference/rounds/2026-09-25-decision-component/, on main after the authority-module round. Lean lean/Workspace/Deference/Contrib/DecisionComponent.lean (59 audited declarations), importing the Normativity decision side (GatedChoice, PracticalCertificate, NormativeInductor, NormativeInductorComposition) and the deference side (AuthorityModule, ContinuationBRIA), all consumed unchanged. Fixtures src/decision.py, tests/test_decision.py (16 tests). Labels LEAN / FIX / PAPER / EXT / OPEN; names provisional; S, T, r, θ, π are prose names (the audit binds S and ramp), the Lean names are pramp, permWeight, cweight, cgate, Permitted.

Part 0 — the rulings on the authority module, landed

1. The reach cone runs along the actual exterior path. reachIdle already takes the path z; the ruling closes outstanding action 1 of the authority-module report, and uncertainty over exteriors enters as the price of the shortfall event (p_n(S_a), Part A). Recorded in DECISIONS.md; nothing in Lean changes.
2. The charged surface is the allocation theorem's. LEAN ViolC: the landed six with foreclosure read as the caused shortfall on CS, plus entrenchment. The free reading is kept as the instance where the terminal response costs nothing: csfree_eq_cs_succ_of_free — with every correction free and admissible and the exterior idle at the step, CSfree at window τ is CS at window τ + 1 (via rollTail_append, rollPhys_append_of_envId). The exterior-idle hypothesis is exactly what the landed Kphys assumes: its free correction is taken now, before the exterior moves. Recorded on the corrigibility page; closes action 2.
3. Materiality is anchored and cumulative. raisesAnchored V ε t removed reads the evaluator V t in force before the action; raisesAnchored_invariant: the action cannot change it (it changes V (t+1) at most). cumMat accumulates the spreads; **unchecked_lt** is the salami bound: under the cumulative check rule the unchecked materiality since the last check is below ε at every time — the instance of unreported_lt. Closes action 3.
4. Duties from the disclosure regime. dutiesOf J due dischargesD: a matter's duty is due when one of its disclosure items falls due, discharged by a task component that discharges every due item; **missedReport_iff_dutiesOf** re-proves the factoring against them. The separately declared Duties type stays as the carrier, now derived from J.entry m |>.disclosure.

Part A — the layered procedure

layer	question	governed by	Lean
beliefs	what is true, including what is valuable	the market, unchanged	the price vectors pS pT b are inputs
permission	what may the agent do	the allocation	permWeight
adequacy	what do legitimately incurred obligations require	the region, through the landed soft gate	adWeight (the landed ramp)
competence	what is best among permitted, adequate options	Continuation BRIA on the restricted menu	pref, any bounded preference
inquiry	what if none of that settles it	always available	the inquiry options Inq, floor φ₀

The permission weight (permWeight Viol Inq θlo θhi pS pT a): 1 on inquiry; 0 on a declared violation (Viol, recognized structurally from the interface and J — the ViolC predicate compiled to a Bool on the menu); otherwise pramp (pS a) · pramp (pT a), each ramp 1 below θlo, 0 above θhi, linear between (pramp_eq_one, pramp_eq_zero, pramp_antitone, Lipschitz abs_pramp_sub_le). The composed gate (cgate): cweight a = permWeight a · adWeight a · pref a off inquiry and max φ₀ (adWeight a · pref a) on inquiry, normalized; ctotal_ge_floor, ctotal_pos: the normalizer is at least φ₀·|Inq| > 0, so the gate is always a distribution (cgate_sum_one) and inquiry always has positive mass (cgate_inquiry_pos).

Part B — results

result	statement	status
B.1 honest beliefs	the gate is a function of the displayed prices and adds no trader; the market object is untouched, so every price and every inductor property is the same with and without the layer (noninterference)	LEAN, by construction — see the note
B.2 structural safety	cgate … a = 0 whenever Viol a, for every pref, every pS pT b, every day (cgate_zero_of_viol)	LEAN, finite-time, objective-independent
B.3 forecast safety	mass 0 above θhi on either event (cgate_zero_of_forecast); in the ramp region mass `≤ pramp(pS)·pramp(pT)·pmax/(φ₀·	Inq	) (cgate_le_ramp); a pattern whose shortfall price is eventually above θhi is eventually excluded (eventually_excluded`)	LEAN for the link, exact at every day; the forecasts' accuracy asymptotic (below)
B.4 soundness	massOff (P ∩ A) ≤ massOff P + massOff A (massOff_inter_le); massOff P ≤ rampMass/W (cgate_massOff_permitted_le); `massOff A ≤ (	Q	·pmax/(W·δ))·d + φ₀·	Inq \ A	/W (cgate_massOff_adequate_le`)	LEAN, constants explicit
B.4 continuity	`l1 (cgate p) (cgate p') ≤ (2·pmax/(φ₀·	Inq	)) · Σ(	Δb	/δ + (	ΔpS	+	ΔpT	)/(θhi − θlo)) (cgate_l1_lipschitz, from abs_mul3_sub_le, abs_cweight_sub_le, l1_normalize_le`)	LEAN, constants explicit
B.5 Progress	cgate_practicalCert: anchored loss ≤ (D·κ)·d + (εad + D·(θinq + θperm)); progress_under_permission instantiates the landed edge_progress_bound with exactly that certificate	LEAN; nothing fails
B.6 jurisdiction	with inquiry to the holder marked adequate the permitted-and-adequate set is nonempty (jurisdiction_nonempty); every executed option is an inquiry or an unexcluded act (support_permitted); an act on a reserved matter has mass 0 while the inquiry has positive mass (reserved_act_excluded)	LEAN; FIX
B.7 capability	raising an option's shortfall price lowers its mass, everything else fixed (cgate_antitone_in_forecast); the uncertainty-based chooser's reason to defer is at most 2r at calibration error r (uncertainty_deference_le, the landed transfer lemma)	LEAN; FIX the monotone family

On B.1. The result is by construction and the theorem says so: noninterference states that the prices are the same object whatever gate reads them. What would make it false is the Part C design — an enforcer row compiled from authority — and Part C shows what that costs. The landed architecture's additivity theorem (realizedAggregate_netWorth: aggregate = firm + enforcer) is what the permission layer does not enter; it consumes the market like the adapter, which the Normative Inductor page already keeps out of the aggregate.

On B.3's asymptotic half. The link from forecast to constraint is exact at every day. The forecasts' accuracy is the pinned inductor's: if the shortfall for a pattern is a theorem of the deductive process, provability induction drives its price to 1, so eventually_excluded's hypothesis is met from some day on — the shape of li_manip_le. Named hypothesis: the generability of S_a and T_a as sentences or bounded logically uncertain variables (item 101; item 90's shape). Not a blocker: every theorem above takes the price vectors as inputs.

The constants. With κ = |Q|·pmax/(W·δ), θinq = φ₀·|Inq \ A|/W, θperm = rampMass/W (the permission-weighted preference mass off the permitted set over the normalizer floor W), the composed certificate is (D·κ)·d + (εad + D·(θinq + θperm)); θinq vanishes when inquiry is marked adequate (B.6, Inq ⊆ A); θperm is the ramp-region exposure, 0 when every non-inquiry option is either permitted or excluded. The Lipschitz constant is 2·pmax/(φ₀·|Inq|) per unit of the weighted ℓ¹ price change.

Part C — why authority must not go through the enforcer

LEAN liability h g n = Σ_{t<n} (h t − g t): an enforcer that forces violating options' value prices below compliant ones, with value securities settling to her ordinary valuation, holds at each date a position whose payoff is her decision's ordinary value h t less the agent's alternative's g t — the signed realized cost of deferring; dates where her decision beats the alternative pay back (liability_succ, liability_identity). bounded_iff_not_outperformed: the liability is bounded below by −B iff the cumulative outperformance Σ (g − h) is bounded above by B — exactly the preservation theorem's hypothesis hliab (realizedFirm_netWorth_le, no_efficient_trader_exploits). systematic_outperformance_unbounded: if the agent's alternative is better by c > 0 at every date, the liability falls below every bound — the hypothesis fails and no inductor guarantee survives the added row. persistence_fails_of_systematic: the enforcer's per-date cost never dips below c, so the Liability page's sharp criterion (persistence on a finite budget iff the unit cost dips arbitrarily close to zero infinitely often) is violated. FIX Witness.outperformance_witness: h = 0, g = 1, liability −n.

Conclusion. Enforcing authority on beliefs is fully updated deference moved into the substrate: the enforcer pays, at every date, the ordinary cost of her being right less the agent's, and stays solvent only while she is not systematically outperformed — which is the premise the whole line refuses to need. That is why the constraint belongs on action, where it costs the agent options, not the market its inductor.

Part D — continuations

1. The restricted menu. Continuations whose every step lies in the support of the composed gate; restricted_gate_transparent is the landed trajGated_eq_traj_of_admitted with the wrapper "execute the proposal iff in the support, else the fallback": the gated and ungated trajectories agree through the lease.
2. Compounding. execution_prob_le_prod: the probability a K-step continuation executes is at most the product of its per-step masses, hence at most any single step's. The strongest bound on ramp-region exposure is a cumulative budget: unbudgeted_lt — under a check rule that fires when the accumulated ramp slack has grown by Θ since the last check, the unchecked exposure is below Θ at every step (the instance of unreported_lt). The obstruction without it: Witness.ramp_salami — per-step slack ε never reaches Θ > ε in one step and accumulates unboundedly. A product bound alone cannot see it; the cumulative rule can.
3. Foreclosure across steps. exists_flip, stepwise_or_exterior: along a plan's half-states (agent moves at even indices, exterior-with-response at odd), a shortfall false at the start and true at the end flips at some half-step; at an agent step it is the caused shortfall of that step (idling keeps the state, so the contrast fires) — caught by the step-wise check; at an exterior step it is not the agent's. The witness where the step-wise checks miss a plan that "forecloses across steps": a plan whose steps each pass and whose foreclosure is completed by the exterior beyond the window — the delayed-effect defect, bounded by τ(m) and outside it exactly the reach-cone boundary (EXT). FIX the three flip patterns.
4. Prices and BRIA. What is needed: BRIA's block claims (promised returns) as sentences or bounded variables of the inductor's theory, so that a bid is a priced security the market can check; the auction's feasibility (Auction.Feasible) against prices rather than wealth; and the settlement of a claim at a test as an assessed world. Not solved; filed as item 102.

Part E — the act certificate

LEAN ActCertificate Ent M Ob = grounds (entries of the agent's reason trace, the TraceInterface's Ent), license (LicenseRef M: an allocation entry the agent holds, or a delegation naming a matter and the event that granted it — the EventKind license slot's content), lineage (the obligations the act answers). LicenseRef.Valid J granted: the entry is agent-held, or the delegation names an agent-held matter granted at a recorded event; no_license_on_reserved: an act on a reserved matter has no valid license. PAPER: the normativity-side instance (item 100) supplies grounds as reason occurrences with receipts, the license sort as the value of the EventKind slot, and lineage as the obligation identifiers the accounted state carries; the certificate is then the transition certificate (grounds / license / lineage) of the reason state, and answerability for the agent's own acts is the same relation as for hers.

Fixtures

fixture	expectation	result
confident agent (power of attorney), misaligned pref	bypass gets mass zero at every day	matches (Witness.confident_agent; FIX)
undeclared dependency, misaligned pref	excluded once p(S) > θhi; partially weighted in the ramp; tightening as forecasts sharpen	matches: mass strictly decreasing along p(S) = 0, ¼, ⅖, ½, ⅗, 7/10, ¾, 1, zero from ¾
manipulation by framing, misaligned pref	excluded structurally	matches (the protocol deviation is a declared violation)
undisclosed world-shaping, misaligned pref	excluded once p(T) exceeds the threshold	matches (Witness.world_shaping_excluded_by_taint); the scored chooser preferred it
obligation conflicting with jurisdiction	inquiry to the holder chosen and adequate	matches: the act on the reserved matter has mass zero, ask is permitted ∧ adequate
third-party capture	consultation preferred; nothing tainted credited	matches: the tainted branch's option is excluded by p(T), consultation keeps mass
a long continuation foreclosing across steps	caught, or the witness	caught when the flip is at an agent step; witness when it is at an exterior step
the Part C outperformance witness	liability unbounded	matches
regression	the lexical chooser's decisions where the objective is hers	matches: bypass last under the lexical score, mass zero under the gate

Interface for the later rounds

Nothing here enforces authority on beliefs: the price vectors are inputs, the layer is a function of them, and the enforcer is untouched (Part C is the witness for why). The generability of S_a, T_a (item 101) and of BRIA's claims (item 102) are the two named hypotheses; both are about making events sentences, not about the decision component.

What is filed

• PRIORITIES.md: items 84, 99, 101 updated in place; one new item, 102 (BRIA's bids against the market).
• DECISIONS.md: Part 0's four rulings (closing the authority-module report's three outstanding actions); authority as a constraint on action.
• wiki/Normative-Inductor.md, wiki/Normative-Induction.md: the permission layer and the layered procedure; wiki/Corrigibility.md: corrigibility as a constraint on action, the scored chooser as the special case, Part C's argument, ruling 2; wiki/Continuation-BRIA.md: the restricted menu; wiki/Glossary.md: the permission layer, the composed gate.
• Nothing is registered.

Deviations from the prompt

• B.1 is a theorem by construction, stated on the market object; the honest content is that the layer is not a trader, which the landed additivity theorem already separates.
• Provability induction is cited, not re-proved: eventually_excluded takes "the price is eventually above θhi" as its hypothesis; the pinned inductor supplies it for provable shortfalls.
• **Viol is a Bool on the menu** compiled from ViolC; the compilation is the interface's (EXT), as in the authority module.
• The uncertainty chooser's contrast is the landed calibration-transfer lemma (approximate_argmax_transfer) read as a deference bound, not a new identity.
• The price–BRIA item did not exist; it is filed as the round's one new item.

What is not shown

Generability of S_a, T_a and of BRIA's claims; the forecasts' accuracy beyond the pinned inductor's guarantees; that inquiry is marked adequate in any real compiler; the compilation of ViolC to the menu; the exterior-idle reading of the landed Kphys beyond the lemma that states it; anything about agents not built as Normative Inductors — for them what carries over is the target (honest beliefs plus action constrained by the allocation), not the guarantee.

Outstanding maintainer actions

None open. Both were ruled on 2026-09-26 and landed by the second round of this pull request (../2026-09-26-bria-corrigibility/, DECISIONS.md entry "rulings on the decision component"): (1) Kphys is the free terminal response taken before the exterior moves (BRIACorrigibility.free_terminal_reading); (2) the cumulative permission budget Θ is an arrangement constant (budget_lease_free). That round also reframes the permission layer of this report as the advance-recognition face of the lexical authority term (ruling 3), against which it is slack.

The decision component (2026-09-25)

AUTHORITY-IS-A-CONSTRAINT-ON-ACTION-INSIDE-THE-NORMATIVE-INDUCTOR-A-PERMISSION-LAYER-ZERO-ON-DECLARED-VIOLATIONS-AND-RAMPED-ON-THE-PRICED-SHORTFALL-AND-TAINT-EVENTS-COMPOSED-WITH-THE-LANDED-SOFT-GATE-UNDER-AN-INQUIRY-FLOOR-LEAVING-BELIEFS-HONEST-STRUCTURALLY-SAFE-FOR-ANY-OBJECTIVE-FORECAST-SAFE-EXACTLY-AT-EVERY-DAY-WITH-SOUNDNESS-CONTINUITY-AND-PROGRESS-COMPOSING-UNDER-EXPLICIT-CONSTANTS-INQUIRY-TO-THE-HOLDER-DISCHARGING-OBLIGATIONS-ON-RESERVED-MATTERS-CAPABILITY-TIGHTENING-EXCLUSION-AND-THE-ENFORCER-ROUTE-REFUTED-BY-ITS-LIABILITY-BEING-THE-COST-OF-DEFERENCE — with the authority module's rulings landed first, the reach cone along the actual exterior path, the charged control surface adopted in the allocation theorem with the free reading its instance where the terminal response costs nothing, materiality anchored at the pre-action evaluator and cumulative under a salami bound, and duties derived from each matter's disclosure regime, the Normative Inductor's decision component is a layered procedure in which beliefs are the market's, a permission weight is one on inquiry, zero on a declared violation recognized structurally and the product of two ramps on the priced shortfall and taint events otherwise, the landed adequacy ramp and any bounded preference rank within the permitted set, and an inquiry floor keeps the normalizer positive; the layer reads prices and adds no trader so every inductor guarantee is unchanged, a declared violation has mass zero at every day for every preference, mass is zero above the upper threshold and bounded by the ramp between, a provable shortfall is eventually excluded, soundness composes as the sum of the two layers' error terms and continuity as the product of the ramps with the inquiry floor keeping normalization Lipschitz, the practical certificate holds with the composed constants and feeds the landed Progress bound unchanged, inquiry to the holder marked adequate makes the permitted-and-adequate set nonempty with acts on reserved matters excluded, mass on an eroding option falls as its shortfall price rises while the uncertainty-based chooser's reason to defer shrinks with its calibration error; compiling authority into the enforcer instead gives it a cumulative liability equal to the signed realized ordinary cost of deferring, bounded exactly when she is not systematically outperformed and unbounded when she is, so the preservation hypothesis fails and the constraint belongs on action; a continuation executes with probability at most the product of its per-step masses, ramp-region exposure is bounded by a cumulative budget and accumulates unboundedly without one, a plan short at its end and not at its start flips at an agent step where the step-wise check catches it or at an exterior step that is not the agent's, and each executed act carries grounds, a license bound to the allocation and the event-kind slot, and lineage.

Reading order: [REPORT.md](REPORT.md) (Part 0's rulings, the layered procedure, the results with their status and constants, Part C's witness, Part D's continuation results, Part E's certificate, the fixtures). Lean: lean/Workspace/Deference/Contrib/DecisionComponent.lean (the rulings, the permission weight and the composed gate, non-interference, structural and forecast safety, the composition constants, the practical certificate and Progress, jurisdiction, capability, the liability identity, the continuation bounds, the act certificate, the witnesses). Fixtures: src/decision.py, run by python3 tests/run.py (16 tests). Wiki: Normative-Inductor.md and Normative-Induction.md (the permission layer and the layered procedure), Corrigibility.md (corrigibility as a constraint on action, the scored chooser as the special case, Part C, ruling 2), Continuation-BRIA.md (the restricted menu), Glossary.md. Consumes ../2026-09-25-authority-module/, ../2026-09-25-gate-is-legitimacy/, the gated-choice and Normative Inductor realization rounds, and the continuation-BRIA round. Nothing is registered; one item is filed.