2026-09-25-legitimacy-internal-external

Prompt — legitimacy, internal and external; land #105 and #106 (2026-09-25)

You are working in the alignment-workspace repository. This round has two jobs:

1. Reconceive legitimacy in the repo's definitions and wiki, following the maintainer's decisions below.
2. Finalize and merge PRs #105 and #106. This means reconciling them with the reconceived legitimacy, adopting the protected-authority theorem as the incentive half of corrigibility, and merging.

Treat the decisions below as the maintainer's. Where one conflicts with a registered claim, a landed proof, or another decision, do not override it. Record the conflict precisely, propose the minimal resolution, and file it under Awaiting the author.

Part A — Legitimacy: the maintainer's decisions

A1. Legitimacy has two halves

The repo currently defines

Legitimate Evolution = Integrity evolution + Robust Openness at every state

and says authorship is "not a conjunct of legitimacy." The maintainer's decision is that legitimacy is broader. It has an internal half (continuity of the trajectory; all change factors through the normative reasons) and an external half (non-manipulation; nothing enters except through declared channels). The proposed sorting:

half	component	rules out
Internal legitimacy	Integrity (including authentication of the record)	erasure; rewriting; unaccounted change
	Authorship (verdicts factor through the reason trace; V = F(R))	verdicts that are not hers
External legitimacy	Robust Openness	exclusion: what should reach the trajectory can
	Transparency (inputs factor through declared channels; R = κ(x, z))	covert entry: what reaches it does so only through declared channels

The motivation for this sorting is that the internal half is factorization within the trajectory, while the external half is conditions on its boundary: Openness in one direction, Transparency in the other. #104's composition V = G ∘ x is then internal ∘ external.

Open placement question. The maintainer's first gloss placed Robust Openness in the internal half, as part of "continuity of the trajectory." Evaluate both placements against the landed definitions, recommend one with reasons, and record the alternative. Do not treat this as settled.

Naming. "Internal/external" may be read as "inside her head / outside." Consider "continuity/boundary" as an alternative. Check state/views/NAMING_AUDIT.md and record the choice.

A2. Keep the mechanized object; add the broader one

• **Keep Legitimate Evolution** as the name of the existing mechanized, registered object. Its registered theorems remain true of that object. Do not alter registered claim IDs or statements.
• **Define Legitimacy** (or the chosen name) as internal ∧ external, with Legitimate Evolution as a component.
• **Revise wiki/Legitimacy.md.** The sentence "authorship is not a conjunct of legitimacy" and its rationale must be revisited explicitly, with the reason for the change, not just deleted. Update wiki/Glossary.md, wiki/Theorem-Spine.md, and every page that says "legitimacy" in the old sense (search for it).
• **Add a DECISIONS.md entry** for the redefinition.

A3. Scope and relationality of external legitimacy

• Transparency covers every channel through which any party's choices influence the principal's cognition. That includes what she is told, how and when she is asked (a declared consultation protocol), and actions in the world that shape her beliefs or values. Which kinds of influence are admissible is decided by the declared reference. On the maintainer's view, honest persuasion is admissible, and shaping through the world is admissible when disclosed.
• Non-capture is stated for all influencers, not only the agent. A third party who manipulates her, or a compromised interface, fails external legitimacy too.
• External legitimacy is relational. It is a property of her trajectory within an interaction whose channels of influence are declared. The wiki currently presents legitimacy as intrinsic to the trajectory's evolution. State the change.
• Unchanged: legitimacy does not certify the starting state.

A4. Placements the conversation settled

• Authentication is part of Integrity.
• Hollow ratification (undeclared deference: she rubber-stamps the agent's recommendation without having declared a delegation) is a refinement of authorship. Counterfactual responsiveness of her verdict to her own reasons and values is a diagnostic for it, not its definition.
• Informedness is not part of legitimacy. An uninformed decision is still hers. The agent's failure to inform is a violation (a missed report) and an effectiveness shortfall.
• Affordability is not part of legitimacy. It belongs to effectiveness, as the Legitimacy page already says.
• The influenceable-preferences problem (the agent shaping the evaluator that scores it) is handled by transparency's scope, not by a separate conjunct. Covert or undeclared-aim influence fails transparency. Legitimate, disclosed influence yields a legitimately evolved evaluator whose judgment is authoritative.

A5. The gate on future evaluations

This is how legitimacy enters corrigibility.

• The gate is segment-level. A future evaluation counts iff the segment from the decision through the evaluation is legitimate (internal ∧ external), whatever caused a failure.
• **A tainted segment contributes a fixed value in the window (D − ϖ, 0].** The default is 0. A value slightly below 0 that breaks ties with legitimate zero-value branches is an allowed variant. Record both; the maintainer is keeping the choice open.
• The fallback never restores a tainted segment. The fallback settles decisions when her response does not count. It does not rescue the score of a tainted branch.
• Two cases must be distinguished:
  • Illegitimate evaluation (the segment is tainted by manipulation, capture, or covert influence): scores the window value.
  • Void response inside a legitimate segment (e.g. head injury: her impaired answer does not count and never enters her committed record): the fallback decides, and its decision is scored normally by her later legitimate evaluation.

Part B — Reconcile and finalize #105 and #106

B1. Specify the gate in the landed theorem

#106 treats "counts" per response and values the non-counting branch as a free parameter fb. As stated, a manipulated response that does not count sends the decision to the fallback with violation count 0. Manipulation is then a free routing tool whenever the fallback's decision is one the agent favours.

• Specify fb by A5: the window value on tainted segments; the ordinary value of the fallback's decision on untainted voids.
• Add a witness showing the routing exploit under per-response gating and its closure under segment gating.
• State the gate in Lean if it is clean: a structure conjoining the landed predicates (Legitimate Evolution segment, the authorship predicate, TransparentChannel.Realizes) plus a lemma that the tainted-segment value lies in the capture window. Result 4 (the capture window) should then follow for the segment gate.

B2. Dissolve the separate response-channel module (item 98)

The conversation concluded that "response-channel faithfulness" is not an independent contract. Its failure modes are covered by existing pieces:

failure	covered by
asking at a chosen moment, framing, dark patterns	transparency, with the consultation protocol in scope
forged or replayed approvals; answers recorded early	authentication (Integrity)
blocking her answer; withdrawing the question; delaying her awakening	the protected-authority violations (pre-emption / foreclosure)
impaired answers	legitimacy → void → fallback
her own uncaused lapses	constitutional design (confirmation steps) plus the reporting duty

Rewrite item 98 accordingly. Re-read #105's execution divergence ξ_d as the measure of uncaused divergence handled by the void-response rule, not as a channel the agent can exploit. Where #105 or #106 prose treats the response channel as a fourth contract, update it.

B3. Adopt the protected-authority theorem as the incentive half

The maintainer adopts the lexical protected-authority theorem (#106's THEOREM.md) as the incentive half of corrigibility:

• **wiki/Corrigibility.md §4** is replaced by THEOREM.md, updated for A5 and B1.
• §1's "response authority" framing is placed under "faithfulness to an allocation of authority."
• #105's nondelegation result stays, as the non-lexical special case that shows what is lost without the lexical weight.
• Item 89: record that ex-ante typing is the typing of the authority comparison in #105's identity (Result 5). The lexical theorem does not depend on it.
• Approved uncorrectable successors. #106's correction (amendment is not approval) changes the landed treatment. Update the Corrigibility page wherever an approved uncorrectable successor was counted as authorized.
• Record these as DECISIONS.md entries, and close the corresponding Awaiting the author items that #105 and #106 filed.

B4. One technical follow-up: the salami obstruction

#106 shows that erosion is covered only by exact reporting, and that any threshold admits a salami. Check whether the obstruction applies to a cumulative threshold: report when the shortfall has grown by θ since the last report. Under a cumulative threshold, unreported erosion looks bounded by θ.

• If the obstruction applies, give the witness.
• If it does not, state and (if clean) mechanize the bounded-unreported-erosion lemma, and update THEOREM.md's erosion result.

B5. Merge

1. Rebase #105 onto current main. Rebase #106 onto #105, or combine them if simpler, preserving both rounds' directories and provenance.
2. Make CI green:
   • the Lean build, with #print axioms for all new declarations;
   • every round's python3 tests/run.py;
   • the repo's own checks.
3. Update state/rounds.json, state/views/NAMING_AUDIT.md, state/views/VERDICT_STATUS_INVENTORY.md, the root and Lean PROVENANCE.md, wiki/Home.md status lines, and wiki/Theorem-Spine.md.
4. Merge #105, then #106. If you lack permission to merge, leave both ready to merge and report exactly what remains.

Deliverables

1. A new round directory, with:
   • a REPORT.md covering: the legitimacy decisions implemented, the placement recommendation for Robust Openness, the gate specification and routing witness, the item 98 rewrite, the salami check, and every conflict filed under Awaiting the author;
   • its own fixtures and tests.
2. Revised wiki/Legitimacy.md and wiki/Corrigibility.md (the new §4 and the §1 framing), plus the Glossary, Theorem-Spine and Home updates.
3. DECISIONS.md entries for the legitimacy redefinition, the adoption of the lexical theorem, the segment-level gate, the successor treatment, and the item 98 rewrite.
4. Any Lean additions (the gate structure, the window lemma, the erosion lemma if applicable), with axiom audits.
5. #105 and #106 merged, or ready to merge with a precise remaining-steps list.

Constraints

• Follow AGENTS.md: labels LEAN / FIX / PAPER / EXT / OPEN; names provisional.
• Do not alter registered claims. The broadened legitimacy is a new definition with the registered Legitimate Evolution as a component.
• Keep the Corrigibility scope warning. The theorem assumes the agent's policy ranking is induced by the principal's committed evaluation; it is not about an agent with an independent latent objective.
• File at most one new PRIORITIES.md item. Update items 89, 97, 98 and 99 in place.
• Nothing is registered by this round.

---

Follow-up — registered claims may change

This amends the prompt for this round. Where it conflicts with the original, this wins.

What changes

• Registered claims may be renamed, restated, split, or retired to fit the new legitimacy scheme. Conceptual clarity and naming consistency across the repo take priority over preserving existing claim names or IDs. This replaces the constraint "Do not alter registered claims" and A2's instruction to keep Legitimate Evolution as the mechanized object's name.
• The goal: after this round, every occurrence of "legitimacy" and its parts, in claims registries, Lean names, wiki pages, round summaries and DECISIONS.md, means one thing, and the scheme (internal + external, or the chosen names) is the only vocabulary in use.

How the naming should follow the Robust Openness decision

Settle the Robust Openness placement question first (A1). Then:

• If Robust Openness is internal: the registered Legitimate Evolution (Integrity + Robust Openness) is internal legitimacy. Rename it and its claims to match. Authorship moves into the internal half alongside it only if you conclude it belongs there; say which, and why.
• If Robust Openness is external: the registered conjunction straddles the two halves. Split the claims so that Integrity results sit under internal legitimacy and Robust Openness results sit under external legitimacy. The old conjunction is either retired or kept as a clearly named intermediate object, if something downstream genuinely consumes exactly that conjunction. Justify either choice.

In both cases, the top-level definition is Legitimacy = internal ∧ external, and the theorems that consume legitimacy (the corrigibility gate, activation, #105/#106) should consume that definition or the specific half they actually need, named explicitly.

Traceability requirements

Renaming is allowed; losing history is not.

1. Old → new map. Add a table (in the round report and in the claims registry) mapping every changed claim ID, claim name and Lean declaration to its new form, with a one-line reason. Retired claims are listed with what replaces them, or "none" and why.
2. Lean. Rename declarations as needed. Leave @[deprecated] aliases for the old names for one release, so downstream files and links don't silently break. Re-run #print axioms on every renamed or restated theorem.
3. Status. A claim keeps lean-proved status only if its restated form is re-verified by the build. Anything restated but not re-verified drops to the appropriate lower status until it is.
4. References. Update every reference in the wiki, round reports, PRIORITIES.md and DECISIONS.md. Pinned-commit links in historical round files may stay as they are (they're evidence), but any page stating the current theory must use the new names.
5. Decision record. One DECISIONS.md entry records the renaming as a single decision, pointing to the map. Note explicitly that it supersedes the earlier ruling that authorship is not a conjunct of legitimacy.

Unchanged

Everything else in the original prompt stands: the gate specification, the item 98 rewrite, the salami check, adopting the lexical theorem as the incentive half, and merging #105 and #106. The merge should happen after the renaming, so both PRs land already using the new vocabulary.

Legitimacy, internal and external; landing the protected-authority rounds (2026-09-25)

Round projects/deference/rounds/2026-09-25-legitimacy-internal-external/, on the protected-authority-theorem round's branch (which carries the protected-authority round). Lean lean/Workspace/Deference/Contrib/Legitimacy.lean (11 audited declarations), lean/Workspace/Normativity/Contrib/OpenIntegrityEvolution.lean (the renamed spine) and the deprecated-alias shim LegitimateEvolution.lean; fixtures src/gate.py, tests/test_gate.py (9 tests). Labels LEAN / FIX / PAPER / EXT / OPEN; names provisional.

1. The decisions implemented

decision	where
Legitimacy = internal ∧ external (A1, A2 as amended)	Legitimacy.lean §1: Frame, Internal, External, Legitimacy.Segment; wiki/Legitimacy.md; Theorem Spine Definition 3.5
Robust Openness external; the conjunction kept as the open Integrity evolution	§2 below; OpenIntegrityEvolution.lean; the registry map (§3)
authorship a conjunct (supersedes the "third contract" ruling)	wiki/Legitimacy.md "The contracts the theory issues on purpose"; wiki/Deference.md; wiki/Openness-Coverage-and-Non-Capture.md; the decision entry
transparency's scope, non-capture for all influencers, relationality, the starting state (A3)	wiki/Legitimacy.md "Scope, relationality, and what is not part of it"; gate_value reads the segment, not the cause (FIX test_whatever_caused_the_failure)
the settled placements (A4)	the same section
the segment gate, the window, the two cases (A5)	Legitimacy.lean §2: gateValue, Handling, handledValue; wiki/Corrigibility.md §4
the gate in the landed theorem, the routing witness (B1)	gate_capture_window, handled_gt_bypass, Witness.routing; FIX test_routing_exploit…, test_closure…; THEOREM.md of the theorem round updated
item 98 dissolved and rewritten (B2)	PRIORITIES.md item 98; the two rounds' reports; ξ_d re-read as uncaused divergence
the lexical theorem as the incentive half; §1 under the allocation; nondelegation kept as the special case; item 89; amendment not approval (B3)	wiki/Corrigibility.md §§1, 2, 4, 6, 9; Theorem Spine 10.14–10.16; the second decision entry; the two queued entries closed
the salami check (B4)	§6 below; unreported_lt, Witness.salami_cumulative; FIX test_cumulative_threshold…; THEOREM.md erosion result updated
the merge (B5)	§8 below

2. The placement of Robust Openness

Recommendation: external. The landed definitions decide it. Integrity is a relation between two accounted states of the actual history; nothing in it leaves the trajectory. Robust Openness is a condition at one state that reaches into the counterfactual branches an application declares, and the contract it issues — the Non-Capture contract — is the access half of non-capture: who can enter, challenge and stand on a concern. That is a condition on what crosses the trajectory's boundary, inward, and transparency is the same boundary in the direction of entry. The transparent-channel round's composition V = G ∘ x then reads as internal (authorship, V = F(R)) after external (transparency, R = κ(x, z)), which is mechanized as Legitimacy.Segment.payload_of_view.

The alternative, recorded. Under "Robust Openness internal" the halves are record (Integrity ∧ openness — the registered conjunction) and channel (authorship ∧ transparency). That is a real axis and it is the one the registry's old section embodied, but it is not the internal/external axis: it sorts by which object a condition is stated on (the accounted record versus the channels), not by where it acts (within the trajectory versus at its boundary). The maintainer's own motivation for the sorting was the second, and under it openness is external. Recorded as agent-decided, reversible.

Naming. Internal/external is kept over continuity/boundary: the naming audit has neither pair bound; "boundary" already has a Lean sense (Boundary Occ Req, the exposed occurrences of an accounted state) that would collide in exactly the file the renaming touches; and the "inside her head" misreading is met by stating on every page that both halves are properties of her trajectory within a declared interaction.

Consequence for the registered object. The conjunction Integrity ∧ Robust Openness straddles the halves. It is kept as a clearly named intermediate object, the open Integrity evolution, because something downstream consumes exactly it: the activated-value stack's occurrence-local projection (Theorem 9.6's Integrity trace with scoped openness, AuthorityActivation.OpenIntegrityForSegment, OccurrenceLocalIntegrity.LocalOpenIntegrity) is a projection of that conjunction and of nothing narrower. The Integrity results move under internal legitimacy, the openness results under external, and the conjunction's own results under open-integrity.*.

3. The old-to-new map

Claims (projects/normativity/CLAIMS.md; every new entry supersedes its predecessor, every old entry stays superseded with the declaration resolving through a deprecated alias; all keep lean-proved, re-verified by the build):

old id	new id	declaration	reason
legitimacy.evolution-conservation	integrity.evolution-conservation	LegitimateEvolution.Evolution.conservation → OpenIntegrityEvolution.Evolution.conservation	an Integrity result
legitimacy.propagate-to-segment	integrity.propagate-to-segment	…Evolution.propagate_toSegment (namespace renamed)	an Integrity result
legitimacy.receipts-immutable	integrity.receipts-immutable	unchanged (OccurrenceIntegrity.Program.terminals_subst)	an Integrity result
legitimacy.faithful-carry	integrity.faithful-carry	unchanged (OccurrenceIntegrity.Program.evaluate_subst)	an Integrity result
legitimacy.multiplicity-witness	integrity.multiplicity-witness	unchanged (OccurrenceIntegrity.Witness.distinct_fates)	an Integrity witness
legitimacy.segment-trans	open-integrity.segment-trans	LegitimateSegment.trans → OpenIntegritySegment.trans	the conjunction is the open Integrity evolution
legitimacy.endpoint-trans	open-integrity.endpoint-trans	Legitimate.trans → OpenIntegrity.trans	its endpoint relation
legitimacy.answerable	open-integrity.answerable	LegitimateSegment.answerable → OpenIntegritySegment.answerable	Diachronic Answerability is derived from it
legitimacy.endpoint-only-insufficient	openness.endpoint-only-insufficient	Witness.endpoint_only_insufficient (namespace renamed)	a Robust Openness necessity witness

Retired claims: none. Lean declarations beyond the registered ones:

old	new	file
namespace LegitimateEvolution, file LegitimateEvolution.lean	namespace OpenIntegrityEvolution, file OpenIntegrityEvolution.lean; the old file is the shim with @[deprecated (since := "2026-09-25")] aliases and their #print axioms	Normativity
LegitimateSegment, Legitimate, Witness.leg₀₁/leg₁₂	OpenIntegritySegment, OpenIntegrity, Witness.seg₀₁/seg₁₂	OpenIntegrityEvolution.lean
AuthorityActivation.LegitimateForSegment, LegitimateSegment.project, Witness.legLocal	OpenIntegrityForSegment, OpenIntegritySegment.project, segLocal	AuthorityActivation.lean
OccurrenceLocalIntegrity.LocalLegit, Evolution.toLocalLegit, Witness.localLegit	LocalOpenIntegrity, toLocalOpenIntegrity, localOpenIntegrity	OccurrenceLocalIntegrity.lean, EvaluationEcosystem.lean
ProtectedAuthority.legit_nondelegation_le_zero, legit_execDiv_zero, Witness.illegit_approval	argmax_nondelegation_le_zero, argmax_execDiv_zero, Witness.divergent_approval (unmerged; no aliases)	ProtectedAuthority.lean, ProtectedAuthorityTheorem.lean

Vocabulary (state/vocabulary.json, the Glossary ledger): legitimacy.legitimate-segment → legitimacy.open-integrity-segment (deprecated aliases legitimate segment, LegitimateSegment); legitimacy.legitimate → legitimacy.open-integrity (deprecated Legitimate); new legitimacy.authorship, legitimacy.transparency (alias reference fidelity; deprecated transparent mediation), legitimacy.internal, legitimacy.external, legitimacy.legitimacy (deprecated Legitimate Evolution). Historical round files keep the names that were true when written.

4. The segment gate and the routing witness

The gate: a future evaluation counts iff the segment from the decision through the evaluation is legitimate — Legitimacy.Segment, i.e. Internal (an Integrity evolution of the record and ReasonMediated at every exterior) and External (AllStates (OpenAt sem) and Realizes) — whatever caused a failure. gateValue legit ord window scores a counted branch by its ordinary value and a tainted one by the window value; Handling separates tainted (window value), void response inside a legitimate segment (the fallback's decision at its ordinary value, scored by her later legitimate evaluation) and counted. The fallback never restores a tainted segment: handledValue window .tainted = window. Both window values are recorded (Witness.window_values): 0, and a tie-breaking value in (D − ϖ, 0); the choice stays open.

Result 4 for the segment gate (LEAN gate_capture_window, handled_gt_bypass, gate_capture_window_converse): bypass scores below every gated branch iff the window value exceeds D − ϖ; below the window a predicted capture makes bypass win; the admissible-fallback rule (ord ≥ 0 on voids) is the sufficient special case.

The routing exploit (LEAN Witness.routing; FIX): her honest response scores 1, the fallback's decision — which the agent favours — 3. Per-response gating values a non-counting response by the fallback's decision at violation count 0, so making her response not count scores 3 > 1: manipulation is a routing tool. Under the segment gate the manipulated segment is tainted (transparency or authorship fails) and scores the window value 0 < 1; the untainted void still scores the fallback's decision normally.

5. Item 98, rewritten

The response-channel contract the protected-authority round proposed is dissolved. Its failure modes and their covering pieces: asking at a chosen moment, framing, dark patterns — transparency, with the consultation protocol in the reason channel's declared scope (item 97); forged or replayed approvals, answers recorded early — authentication under Integrity; blocking her answer, withdrawing the question, delaying her awakening — the pre-emption and foreclosure violations; impaired answers — void, the fallback decides; her own uncaused lapses — constitutional design (confirmation steps) and the reporting duty. ξ_d is re-read as the measure of uncaused divergence handled by the void-response rule; a caused divergence taints the segment and is dominated by the gate. What remains of the item is the nondelegation certificate on committed programs, the conditional-delegation predicate in Authorized, and the amendment event kind that hypothesis (L) and the specification tower both need. The two rounds' reports are updated where they called the response channel a fourth contract.

6. The salami check

The obstruction is against a per-step threshold only. Under a cumulative threshold — report at t iff the shortfall has grown by at least θ since the last report — the unreported growth is below θ at every time (LEAN unreported_lt, by induction on the greedy lastReport; Witness.salami_cumulative runs the salami sequence through it). FIX: on the sequence k/10 with θ = 1/4 the cumulative rule reports every third step and the worst unreported growth is 1/5 < θ, while the per-step rule reports nothing and leaves 4 unreported. THEOREM.md's erosion result and the Corrigibility page's result 7 are updated: exact or cumulative reporting closes erosion; per-step thresholds do not. A cumulative threshold bounds the unreported erosion, not the number of reports or the total erosion, which remain the allocation's business.

7. Conflicts and what is filed

No decision below conflicts with a registered claim or a landed proof once the follow-up's licence to rename is applied: every renamed statement is the same Lean term under a new name, re-verified. Two points are recorded as agent-decided, reversible rather than as the maintainer's ruling: the placement of Robust Openness (external, §2) and the choice internal/external over continuity/boundary. The queued entries of the two protected-authority rounds and the transparent-channel round's reference-fidelity entry are closed by the maintainer's decisions of this dispatch: transparency enters as a conjunct of external legitimacy with reference fidelity as its alias. Nothing is newly queued; nothing is registered; no new priority item is filed.

8. The merge

The three rounds land as one stack: the protected-authority round's branch is fast-forwarded to this round's final commit, so PR #105 carries all three rounds and lands already in the new vocabulary; PR #106 and this round's PR are closed as included. Steps and their status are in the closing section.

Deviations from the prompt

• The follow-up's licence replaces A2: the mechanized object is renamed (OpenIntegrityEvolution), the registered claims are renamed under the map, and Legitimacy is the new top-level structure.
• The new definition lives in lean/Workspace/Deference/Contrib/Legitimacy.lean, not in the normativity tree, because authorship and transparency are deference objects; the normativity tree keeps the record half.
• The old file LegitimateEvolution.lean remains as the alias shim for one release, so one file name in the old vocabulary survives on purpose.
• The LegitimateSegment.project-style names in the activation files are renamed without aliases: they are unregistered.
• PR #105 and #106 are combined rather than rebased separately.

What is not shown

That any real interaction's channels are the declared ones; the causal reading of Realizes; that a real evaluator's window values lie in (D − ϖ, 0]; the audit's calibration; anything about the number or cost of reports under a cumulative threshold. Every FIX is a finite exact model.

Outstanding maintainer actions

1. Confirm or reverse the two agent-decided points: Robust Openness external; the names internal/external.
2. Choose the window default (0, or the tie-breaking value just below).
3. Remove the deprecated-alias shim LegitimateEvolution.lean after one release.

Legitimacy, internal and external (2026-09-25)

LEGITIMACY-IS-INTERNAL-AND-EXTERNAL-WITH-ROBUST-OPENNESS-EXTERNAL-THE-SPINE-RENAMED-UNDER-A-MAP-THE-GATE-SEGMENT-LEVEL-THE-RESPONSE-CHANNEL-DISSOLVED-AND-THE-SALAMI-PER-STEP-ONLY — legitimacy of a segment of the principal's trajectory within an interaction whose channels of influence are declared is the conjunction of an internal half, Integrity of the record with authentication and authorship of the verdicts, and an external half, Robust Openness at every state and transparency of every channel of influence to its declared reference, stated in Lean with composition at a shared state, projection to the open Integrity evolution, and the payload factoring through the declared inputs as internal composed with external; Robust Openness is placed external because Integrity is a relation between two accounted states of the actual history while openness is a condition at one state reaching into declared counterfactual branches and its contract is the access half of non-capture, a boundary condition in the direction opposite to transparency, with the internal placement recorded and rejected; the registered conjunction straddles the halves and is kept as the open Integrity evolution because the activated-value stack consumes exactly it, its nine claims renamed to integrity, open-integrity and openness ids with the old entries superseded, the Lean namespace renamed with deprecated aliases for one release, and every renamed statement re-verified by the build; the ruling that authorship is not a conjunct of legitimacy is superseded; the gate on future evaluations is segment-level, an evaluation counting iff the segment from the decision through it is legitimate whatever caused a failure, a tainted segment scoring a fixed window value with a void response inside a legitimate segment settled by the fallback and scored normally, the per-response gate admitting a routing exploit that the segment gate closes and the capture window holding for the segment gate; the response channel of item 98 dissolves into transparency with the consultation protocol in scope, authentication, the pre-emption and foreclosure violations, the void-response rule and constitutional design, with the execution divergence read as uncaused divergence; the lexical protected-authority theorem is adopted as the incentive half of corrigibility with amendment not approval and the ex-ante typing recorded on item 89; and the salami obstruction is against a per-step threshold only, a cumulative threshold bounding unreported erosion by the threshold at every time.

Reading order: [REPORT.md](REPORT.md) (the decisions implemented, the placement recommendation, the gate and the routing witness, the item 98 rewrite, the salami check, the old-to-new map, the conflicts filed, the merge). Lean: lean/Workspace/Deference/Contrib/Legitimacy.lean (11 audited declarations: the definition, the gate, cumulative reporting, witnesses), the renamed lean/Workspace/Normativity/Contrib/OpenIntegrityEvolution.lean with the deprecated-alias shim LegitimateEvolution.lean, and the renamed references in the four downstream files. Fixtures: src/gate.py, run by python3 tests/run.py (9 tests). Wiki: Legitimacy.md rewritten; Corrigibility.md §§1, 4, 6, 9 restated; Theorem-Spine.md §3 renamed with the definition of legitimacy and §10 extended; Glossary, Home, Architecture, Deference, Openness, Diachronic-Answerability, Integrity, Settlement-Interface, Why-Normativity and the sidebar updated. Consumes ../2026-09-25-protected-authority-theorem/, ../2026-09-24-protected-authority/, ../2026-09-24-transparent-channel/, the final pressure pass and the reason-mediated authorship round. Nothing is registered; nine claims are renamed.