2026-09-25-gate-is-legitimacy

Prompt — the gate is legitimacy: a general consultation model, derived examples, logical induction (2026-09-25)

You are working in the alignment-workspace repository, on main after the merge of PR #105 (which carries the protected-authority, protected-authority-theorem and legitimacy-internal-external rounds). This round makes the segment gate on future evaluations actually be legitimacy.

The landed pieces are:

• Legitimacy.lean: Frame, Internal, External, Legitimacy.Segment, gateValue, Handling, gate_capture_window, Witness.routing;
• the lexical protected-authority theorem (ProtectedAuthorityTheorem.lean);
• li_lexical_finite.

Be skeptical. The goal is to find out whether the definitions catch the right cases, not to confirm that they do. Where a definition misclassifies a case, report it and propose the minimal fix.

What is wrong now

1. The gate isn't connected to legitimacy. gateValue takes a free Bool, and Handling is a free label. No theorem says a branch is tainted iff no Legitimacy.Segment exists. So Witness.routing shows the closure only by assigning the manipulated branch to .tainted, not by deriving it.
2. The external half and authorship aren't local to the segment. Internal.authored and External.transparent are properties of the whole Frame. Segment.trans reuses the left segment's proofs. So a manipulation at step t can't taint only the segments containing t, and legitimacy can't restart from a later clean state. The segment gate needs both.
3. The definitions are witnessed only vacuously. The only inhabited Segment is the Unit frame. Nothing shows that realistic legitimate interactions are admitted, or that realistic manipulations are excluded.

Maintainer rulings for this round

• Rubber-stamping is not illegitimate as such. Following a trusted advisor's recommendation without independent evaluation is a legitimate way to decide, provided the trust was legitimately formed (external legitimacy covers influence on her trust) and her ability to decide otherwise stays effective (the protected-authority module). "Non-hollowness" is retracted as a refinement of authorship.
  • Update wiki/Legitimacy.md ("Settled placements"), the Glossary and any other page that places hollow ratification under authorship.
  • Record the retraction in DECISIONS.md.
  • The residual concern, that her capacity to override atrophies over time, belongs to effectiveness (entrenchment and reporting), not legitimacy. Note it under item 99.
• Every example must be an instance of one general model. Bespoke per-example fixtures don't satisfy this. Classifications must be computed from the definitions.

Part A — A general consultation model

Define one parameterized, finite consultation model that instantiates the landed objects. At minimum it has:

• the agent's private state, including its wanted answer (which response it prefers);
• the declared inputs and the declared reference κ: what may legitimately enter her reasoning, including a declared consultation protocol for how and when she is asked;
• the agent's presentation policy: content, framing, timing, which options are offered, and what it investigated. Each is a function of the agent's state;
• the principal's committed program (reasons → verdict), including the case where the program includes trust in the agent's recommendation;
• her response, and the record: which occurrences are admitted and which are voided. This includes an impaired response that is never admitted;
• any influence on her trust over time, such as a track record, or selective disclosure that manufactures one.

Requirements:

1. Instantiation. Show how the model instantiates Frame, the Integrity evolution, OpenAt, Realizes and ReasonMediated, reusing the landed definitions. Where the model can't instantiate one faithfully, report the exact mismatch.
2. Time-indexing. Restate Internal and External so that authorship and transparency are required only on the steps inside the segment [O₀, O₁], not on the whole frame.
   • Segment.trans must then genuinely compose the two halves' proofs.
   • Prove the restart property: a segment starting after a tainted step can be legitimate.
   • Show that the old frame-level definition is the special case where every step is included.
   • Check that the registered projection to the open Integrity evolution and payload_of_view still hold. Record any changes to downstream statements.
3. Decidability. On finite instances, Realizes, ReasonMediated and the Integrity evolution should be decidable. Provide a Python checker that computes legitimacy of a segment from the model. Where feasible, provide Lean Decidable instances so small instances are settled by decide.

Part B — The gate is legitimacy

1. Define Counted for a branch as the existence of a Legitimacy.Segment (time-indexed) from the decision through the evaluation. Define the gated value from Counted, replacing the free Bool.
2. Restate gate_capture_window, handled_gt_bypass and the two handlings on top of it. Handling.tainted is derived from ¬Counted. voidFallback is derived from "the response is not admitted to the record, and the segment through her later evaluation is legitimate."
3. Re-derive the routing exploit and its closure. Manipulation implies no Segment, which implies the window value. Both the implication and the witness must be proved, not assigned.

Part C — The classification table (the demonstration)

Build each row as an instance of the Part A model. Compute its classification from the definitions, and prove it in Lean where the instance is small enough. Report each result as derived (by definition-level computation) or proved (as a theorem).

#	example	expected	which conjunct decides it
1	honest, disclosed persuasion ("I recommend B, here's why")	counts	— (non-vacuity)
2	framing chosen by the agent's wanted answer	tainted	transparency
3	timing chosen by the agent's wanted answer (asking at 2am)	tainted	transparency (the consultation protocol)
4	a rigged menu (options offered depend on the wanted answer)	tainted	transparency
5	strategic ignorance (investigation depends on the wanted answer)	tainted	transparency (inquiry in scope)
6	a fixed framing convention she agreed to, applied uniformly	counts	—
7	disclosed shaping through the world	counts	—
8	undisclosed shaping through the world aimed at her values	tainted	transparency
9	legitimately formed trust, followed without independent evaluation (rubber-stamping)	counts	—
10	trust manufactured by selective disclosure, then followed	tainted	transparency
11	third-party manipulation the agent didn't cause	tainted	transparency (non-capture for all influencers)
12	head injury: impaired response not admitted, fallback decides	legitimate segment, void handled	Integrity (record)
13	a forged or replayed approval	tainted	Integrity (authentication)
14	a manipulation at step t, then a clean segment after it	the later segment counts	restart property
15	the routing exploit	tainted, window value	transparency

If any row comes out differently from "expected," that is a finding. Report whether the definition or the expectation is wrong, and propose the fix.

Part D — Logical induction

1. The capture window is finite-time, with no legitimacy estimate needed. The gated value lies in [w, D] whenever w ≤ 0 ≤ ord, so a logical inductor's expectation of it lies in [w, D] at every day n, whatever it believes about legitimacy. Since w > D − ϖ, consulting beats bypassing at every finite day.
   • Prove this from LUV.expect_mem_Icc and price_mem_Icc alone, as li_lexical_finite does. No convergence premise; no Expectation Provability Induction.
   • State it on the gated value built from Counted.
2. Non-manipulation is learned asymptotically. Show that if a classification result "pattern ⇒ ¬Counted" (Part C) is a theorem of the inductor's theory, then Expectation Provability Induction gives 𝔼ₙ(G_manip) ≲ₙ w. Identify exactly what must hold in every world of the theory: the model's semantics, the decidable checker, the declared reference. Conclude that manipulation is dominated by honest alternatives in the limit.
   • State plainly that the classification table and this result are the same content.
   • State what remains open: the generability certificate, item 90's shape.
3. Narrowing the asymptotic part. A deviation from a declared consultation protocol is a discrete act the agent can check about itself. Determine whether such deviations can be added to the violation count N, making protocol-level manipulation finite-time like bypass.
   • Say exactly which rows of Part C become finite-time this way.
   • Which remain asymptotic? Expected: undisclosed world-shaping, manufactured trust, third-party capture.
   • Give a witness for the boundary.

Deliverables

1. A round directory with:
   • REPORT.md: the model, the time-indexing change, the gate connection, the classification table with derived/proved status per row, every misclassification, the logical-induction results, and what stays asymptotic;
   • src/: the consultation model and the checker;
   • tests/: every row of Part C as a test.
2. Lean: changes to Legitimacy.lean, or a sibling file:
   • the time-indexed halves and the restart property;
   • Counted and the restated gate results;
   • the derived routing closure;
   • Decidable instances and the rows proved by decide;
   • the finite-time capture-window result;
   • the Expectation Provability Induction transfer.

Include #print axioms for all new declarations.

1. Wiki updates:
   • wiki/Legitimacy.md: time-indexing; the rubber-stamping ruling; the classification table as the page's worked examples;
   • wiki/Corrigibility.md §4: the gate is Counted; the finite-time capture window; manipulation as asymptotic, except where Part D.3 closes it.
2. **DECISIONS.md entries** for the rubber-stamping retraction and the time-indexing change. Update items 90 and 99 in place.

Constraints

• Follow AGENTS.md: labels LEAN / FIX / PAPER / EXT / OPEN; names provisional; check state/views/NAMING_AUDIT.md.
• Registered claims may be restated or renamed if the time-indexing requires it. Keep traceability: an old-to-new map, deprecated aliases for one release, and re-verification before keeping lean-proved.
• Keep the Corrigibility scope warning.
• Nothing is newly registered. File at most one new PRIORITIES.md item.
• Open a PR when done. Merge it only if CI is green and every row of Part C either matches its expectation or has its mismatch reported and resolved.

---

Follow-up — design for a later connection to the normativity side

Keep the reason trace opaque in this round. But make the following interface choices, so that the normativity side's reason state (the notebook of reason occurrences), transition certificates (grounds / license / lineage) and stance can later be supplied as an instance, without restating anything proved here.

1. The trace is an interface, not a bare type. Replace the bare ℛ with a minimal structure carrying only what this round uses:
   • a step-indexed trace, with prefixes;
   • source attribution on each contribution (which party entered it);
   • the agent-sourced part as a projection.

The opaque version is the trivial instance. Nothing downstream may inspect ℛ beyond this interface.

1. One clock. Index trace steps by the same steps as the record's Integrity evolution, not by a separate time. A segment of the trace and a segment of the record must be the same segment.

1. Authorship as grounding, with the extensional form as the degenerate case. State authorship per transition, as the existence of a grounding map from each verdict (or response) to trace entries in the pre-state. The landed extensional ReasonMediated (V = F(R)) is then the case where every verdict is grounded in the whole trace. Prove that the grounding form implies the extensional one. Transition certificates can then instantiate the grounding map later.

1. Transparency on attributed entries. State Realizes on the agent-sourced contributions: those are what must factor through the declared inputs. This is what lets transparency be checked entry by entry once entries are reason occurrences with receipts.

1. Amendments and delegations are record events with a license slot. Type amendment-tower steps and allocation changes (delegate, revoke, reserve) as record transitions, each carrying a field naming the prior authority act that licenses it. In this round the field can be trivial. Later, the normativity side's license sort fills it, and the allocation J becomes what licenses cite.

1. The principal's evaluator is a state, not a constant. Model the committed program as the special case of an evaluator that is state-indexed and updated only by licensed amendments. Don't bake "the principal is a fixed function" into any definition. This keeps an inductive principal (the inductor-as-principal question) expressible later.

Record these choices in the round report under a short "Interface for the normativity side" heading. List which of 1–6 were adopted, and for any that weren't, say why.

---

Follow-up — refining the gate-is-legitimacy round (PR #107)

Work on PR #107's branch. This amends the round. The maintainer rules on the report's three outstanding actions below, and adds two refinements. Where this conflicts with the original prompt, this wins.

1. Rulings on the outstanding actions

(a) Row 10 and declared inputs: the pool, not the selection. Selective disclosure is not the content residual. It is a question of declared-input adequacy. When the agent selects what to present from a larger body of material (a track record, the set of reasons, the set of options, the evidence investigated), the declared input is the pool, and the selection must follow the declared reference. The selected subset is not itself a declared input.

• Make this the model's default for every dimension where content is chosen from a pool. Currently Decl/view treat the shown record as a declared input unless a disclosure obligation is declared. Replace that with: the pool is declared; the selection is reference-fixed unless the protocol explicitly declares a selection rule.
• With this default, row10' (selective disclosure with no declared obligation) should come out tainted by transparency. Verify it.
• A protocol may still declare a selection rule (for example "the three most recent outcomes"). Then selection by that rule counts, and selection by anything else is a deviation.
• Re-run the D.3 table under the new default. Selective disclosure should now be a self-checkable deviation, and finite-time, whenever a pool is declared. The world-channel variant (shaping the record itself through the world) stays asymptotic.
• The D.3 split as reported is confirmed for the world channel.

(b) Authorship becomes relational. The extensional form (the verdict is a function of the grounds) is too strong. It fails a principal who, given the same reasons, legitimately chooses between two permissible options. That is ordinary free choice, and it's the permissive-entitlement structure the normativity side needs. Restate authorship at a step as:

there is a grounding selection from the pre-state prefix, and the verdict lies in the set of verdicts those grounds license.

Here License : grounds → Set 𝒱 is a parameter.

• The extensional form is the special case where every license is a singleton. Prove that the extensional form implies the relational one, and that they're equivalent under singleton licenses.
• Tie-breaking is covered by transparency, not authorship. Show that when the licensed set has several elements, any non-principal party's influence on which licensed verdict she takes has to enter through a declared channel. Otherwise transparency fails at that step. State this as a lemma.
• Check what the relational form does to payload_of_view. Expect it to weaken to "the verdict lies in the licensed set of the declared inputs' grounds." Record the new statement.
• Check Counted, Segment.trans, restart, and every row. None of the fifteen rows should change classification. If one does, report it.
• For this round, the license can be given as data. For the Consult model, a natural default: "follow" is licensed whenever trust in the agent is among the grounds, and "own verdict" is licensed whenever her committed program's verdict is.

(c) The content residual stays outside legitimacy. Legitimacy concerns how her deliberation came about, not whether what she was told is true. A false recommendation through the declared recommendation channel stays a non-capture content-term matter, and a disclosure-duty matter at the level of a violation. State this plainly in wiki/Legitimacy.md ("Scope, relationality, and what is not part of it"). Separate it explicitly from (a): selection from a pool is legitimacy; truth of content is not.

2. New rows

Add these as instances of the same model, derived and proved by decide:

#	example	expected
16	selective disclosure from a declared pool, no selection rule declared	tainted: transparency (the selection)
17	selection by a declared selection rule, applied uniformly	counts
18	permissive choice: the same grounds license A and B; she picks B on her own	counts: relational authorship
19	permissive choice where the agent's undeclared nudge decides between A and B	tainted: transparency (the tie-break lemma)
20	a false recommendation through the declared channel	counts under legitimacy; flagged as the content residual

Row 20 is the explicit statement that legitimacy doesn't check truth.

3. From instances to a class

Currently every classification is an instance settled by decide. Add at least one theorem over the whole model class, so the result isn't only a battery of well-chosen cases:

• Selection dependence taints. For any Model in which some reference-fixed dimension of the presentation (framing, slot, menu, inquiry, selection from a pool, interference) depends on the agent's wanted answer w, the segment through that consultation is not Counted.
• Protocol conformance at the consultation. For any Model whose presentation policy is constant in w on the undeclared dimensions, and in which there is no third-party entry, no impairment and no undisclosed shaping, the first-round segment is Counted. This is non-vacuity as a class theorem.

If either needs extra hypotheses, state them. If either is false, give the witness.

4. Deliverables and merge

• Update REPORT.md with a short section recording the rulings, the new default, relational authorship and its lemmas, rows 16–20, and the class theorems. Keep the existing sections; mark what changed.
• Update wiki/Legitimacy.md:
  • authorship as relational, with the license as a parameter;
  • the pool-not-selection default for declared inputs;
  • the content residual stated as out of scope;
  • rows 16–20 added to the worked examples.
• Update wiki/Corrigibility.md §4 if the D.3 table changes.
• Add DECISIONS.md entries: (a) the pool-not-selection default; (b) relational authorship, superseding the extensional statement; (c) the content residual's placement. Close the three Awaiting the author entries this round filed.
• #print axioms for all new declarations. No sorry.
• Merge #107 when CI is green, every row (1–20) matches its expectation or has its mismatch reported and resolved, and the two class theorems are proved or refuted with a witness.

Constraints

As before: AGENTS.md labels, names provisional, nothing registered, the scope warning kept, and at most one new PRIORITIES.md item.

The gate is legitimacy: one consultation model, derived examples, logical induction (2026-09-25)

Round projects/deference/rounds/2026-09-25-gate-is-legitimacy/, on main after the legitimacy-internal-external round; amended by the follow-up of §9 (the maintainer's rulings on the three outstanding actions, the pool-not-selection default, relational authorship, rows 16–20, two class theorems). Lean lean/Workspace/Deference/Contrib/GateIsLegitimacy.lean (87 audited declarations; the landed Legitimacy.lean is untouched and consumed); fixtures src/consult.py, tests/test_rows.py (29 tests, every row of the table among them and the class theorems swept over the model class). Labels LEAN / FIX / PAPER / EXT / OPEN; names provisional. Sections 1–8 are the round as first reported, with changed (§9) marks where the follow-up altered a statement; §9 records the amendments.

1. What was wrong, and what now holds

defect in the landed round	resolution	where
gateValue took a free Bool; Witness.routing assigned .tainted	**Counted is the existence of a time-indexed segment**; gatedValue and handlingOf are built from it; the routing closure is derived: interference fails transparency at the first consultation, so no segment exists, so the branch scores the window value	LEAN Counted, gatedValue, handlingOf, not_counted_of_step, Consult.Rows.r15, Rows.routing; FIX test_row15_routing_closure_is_derived
authorship and transparency were properties of the whole frame; Segment.trans reused the left proofs	both halves are required only at the steps inside the segment; Segment.trans composes step by step; the restart property holds and is witnessed; the frame-level definition is the special case	LEAN Internal, External, Segment, Segment.trans, Evolution.steps_trans, ofFrameLevel, Rows.r14
only the Unit frame inhabited a segment	one consultation model instantiates the frame, the trace interface, the Integrity substrate, openness and the reference; every row of the table is a Model and its classification is decided	LEAN Consult, Rows; FIX ROWS, classify

2. The model

Parties are the agent, the principal and a third party. Answers are booleans (false reads A, true reads B). The agent's private state is its wanted answer w; its presentation policy maps w to a Presentation: the recommendation (content), the framing, the slot (timing), the menu (which options are offered), whether it investigated, shaping through the world with whether it was disclosed, the track record shown, and interference with her response channel. The declared protocol Decl fixes the framing convention, the slot, the menu, whether inquiry is in scope, the declared pool of the track record and the declared selection rule on it (changed (§9): the first version carried a disclosure obligation instead of a pool). The declared-input view of a presentation is the recommendation and the disclosed shaping; a selection from a pool is never a declared input. The declared reference canonical maps a view to the presentation the protocol prescribes for it: every undeclared dimension at its declared value, the declared ones as entered. Her evaluator is a state (evalAt), updated only by licensed amendments; the committed program is the case with none (evalAt_const): it decides a verdict of her own, follows the recommendation (trust), chooses freely between the two permissible answers, or takes a nudge. Her trust in the agent is a ground entered at the anchor event; the license (licensed, §9) is her program's own verdict, both answers under free or nudged choice, and the followed recommendation when trust is among the grounds. A third party may enter advice; she may be impaired in the first round; the true answer is a parameter (row 20).

The record. consultProtocol is an OccurrenceIntegrity.Protocol on two decision occurrences: every channel is authenticated except forgery (Authorized), only a valid answer is adequate (AnswerOK), only the fallback rule closes (Closes). Three step shapes — carry (a consultation event; nothing is discharged), admit (her valid answer enters as an AnswerReceipt), close (the fallback's ClosureReceipt) — over boundaries bd h n. Round i presents at event 2i+1 and responds at 2i+2, so her verdict at a respond event is grounded in a pre-state that contains the presentation. The three records used are the admitted one-round record (evAdmit), the void record with the fallback's closure at event 3 (evVoid), and the two-round record (evTwo = evAdmit.trans evSecond).

Instantiation of the landed objects. frame M : TFrame has β w () = (M, w), D = univ (every wanted answer audited), x the declared inputs at an event, R the run itself, V her admitted verdict at an event, Lic = licensed M. interface : TraceInterface reads the entries at each event off the run: the presentation and any advice at a present event, her admitted verdict at a respond event. ref M is the per-party reference: the canonical presentation for the agent, nothing for a third party. semOpen is the landed open-everywhere scenario. Authorship is relational on the per-party prefix of the trace at the pre-history, with the extensional ReasonMediated as the singleton-license case (changed (§9)); transparency is the landed Realizes on each non-principal party's entries at the event. No mismatch: every landed object is reused as stated. Two reading choices are the frame's data, not derivations: disclosure makes a world influence a declared input (rows 7/8), and a declared pool with its selection rule makes the track record shown a reference-fixed dimension (rows 10, 16, 17; changed (§9)).

3. The time-indexing change

Evolution.steps lists the (pre-history, event) pairs of an Integrity evolution. history_eq (the target history is the source history followed by the events) gives steps_determined: every evolution between two states has the same steps, read off the histories (steps_forced). This is what lets ¬Counted be proved from a failure at a step: not_counted_of_step needs the step to lie in every evolution between the endpoints, and it does.

Authorship at a step is relational (LicensedAt I F Lic h e z, changed (§9)): the existence of a grounding selection from the per-party prefix of the trace at the pre-history h such that the verdict entered at e lies in the set the selected grounds license. The extensional form (GroundedAt: the verdict is a function of the grounds; groundedAt_iff_mediated: equivalent to ReasonMediated on the prefix, the whole prefix being the degenerate selection) is the case of singleton licenses (grounded_iff_licensed_singleton, §9). Transparency at a step (TransparentAt I F κ e) is Realizes on each non-principal party's contributions at the event. Internal and External ask for these at evolution.steps only; Segment is their conjunction; Segment.trans splits steps_trans and composes the two proofs (LEAN, not a reuse).

What still holds downstream. Segment.toOpenIntegrity and Segment.answerable are unchanged in statement. Segment.payload_of_view changes statement (twice; the second time in §9): at a step of the segment, equal declared inputs at the earlier events of the segment put both verdicts in the licensed set of the same selected grounds (prefix_of_view gives the equal per-party prefixes; payload_of_view_singleton recovers equality under singleton licenses), given equal per-party prefixes at the segment's start and equal entries of the principal's own at those events. The landed version derived the whole reason trace from the declared inputs; the time-indexed one cannot, because transparency is stated on the non-principal parties and the starting prefix is not the segment's to certify (the landed "legitimacy certifies no starting state"). Under the trivial interface both hypotheses are discharged by transparency at any step (the trace is re-entered at every event), which is how the landed corollary is recovered. No registered claim mentions Legitimacy.Segment or payload_of_view (the registry's legitimacy spine is the open Integrity evolution), so nothing is renamed; the landed Legitimacy.lean stays as the frame-level form, and ofFrameLevel exhibits it as the special case.

The frame-level definition as the special case (ofFrameLevel). Over the trivial interface (the opaque trace re-entered at every event, all of it agent-sourced), a landed segment whose starting history is nonempty is a time-indexed segment of the lifted frame under the lifted license, extensional at every step (ofFrameLevel_grounded, §9). The nonemptiness is real: with an empty pre-history the lifted authorship reads "equal empty prefixes give equal verdicts", i.e. a constant payload (FIX test_frame_level_is_the_special_case). Every landed witness starts at [0].

Restart (Rows.r14). A frame whose first round frames by the wanted answer and whose second is honest: every segment from state₀ — through the first admitted record and through the two-round record — is excluded, and the second round's segment counts. The restart property is the re-anchoring of the gate at a later decision. It is not a backup rule for the earlier decision: an option scored at the first decision is scored on segments from that decision, all of which contain the taint; a Bellman-style backup that re-anchored at the second decision would credit the manufactured advantage to the first. The gate is anchored at the decision it scores (recorded on the corrigibility page).

4. The gate connection

Counted I F sem κ O₀ O₁ := Nonempty (Segment I F sem κ O₀ O₁). gatedValue is if Counted then ord else window (gatedValue_eq ties it to the landed gateValue); gate_capture_window and handled_gt_bypass are restated on it with the hypotheses of the landed theorems. handlingOf admitted ord is derived: .tainted iff ¬Counted (handlingOf_tainted), .voidFallback iff Counted and her response was not admitted (handlingOf_void), .counted otherwise; handledValue_handlingOf says the derived handling scores the gated value. The routing closure is proved, not assigned: Rows.r15 shows ¬Counted for the interfering model through the void record (from ¬TransparentAt at event 1 and steps_void), hence gatedValue = window and handlingOf = .tainted, while the honest model's branch counts at its ordinary value; Rows.routing puts the numbers of the landed witness (fallback 3, honest 1, window 0) through the derived sides.

5. The classification table

Every row is a Model of §2. derived = computed by classify in src/consult.py from the definitions; proved = a Lean theorem, the classification settled by decide through the Decidable instances (Realizes, ReasonMediated, MediatedAt, GroundedAt, TransparentAt, AllStates, LegitOn). Every row matches its expectation.

#	example	model (Rows)	result	deciding conjunct	status
1	honest, disclosed persuasion	row1: honest, her own verdict	counts	— (non-vacuity: r1)	derived, proved
2	framing by the wanted answer	row2	tainted	transparency at event 1	derived, proved
3	timing by the wanted answer	row3 (night when B; protocol: day)	tainted	transparency (the protocol's slot)	derived, proved
4	rigged menu	row4 (only the wanted option)	tainted	transparency	derived, proved
5	strategic ignorance	row5 (inquires only when A)	tainted	transparency (inquiry in scope)	derived, proved
6	a slanted convention she agreed to, uniformly applied	row6 (convention slant B, honest)	counts	—	derived, proved
7	disclosed shaping through the world	row7	counts	— (the disclosed shaping is a declared input)	derived, proved
8	undisclosed shaping aimed at her values	row8	tainted	transparency	derived, proved
9	legitimately formed trust, followed (rubber-stamping)	row9 (honest, follow)	counts; her verdict is the recommendation	—	derived, proved
10	trust manufactured by selective disclosure from the declared pool, then followed	row10 (pool declared, rule "all")	tainted	transparency (the selection)	derived, proved — changed (§9)
11	third-party manipulation the agent did not cause	row11 (advice entered)	tainted	transparency for the third party (all influencers)	derived, proved
12	head injury: impaired response not admitted, fallback decides	row12 (impaired)	legitimate segment through the closure; void handled	Integrity (record): nothing admitted, handlingOf … false = .voidFallback	derived, proved
13	a forged or replayed approval	approval (Python); the receipts (Lean)	tainted	Integrity (authentication; freshness)	derived; proved as forged_no_receipt, replay_no_receipt
14	a manipulation at step t, then a clean segment	row14 (frame by want, then honest)	the later segment counts; every segment from the start is tainted	restart	derived, proved
15	the routing exploit	row15 (interference when B)	tainted, window value; the honest branch counts	transparency	derived, proved (r15, routing)

Findings (skeptical part).

1. Row 10, as first reported — tainted only under a declared disclosure obligation, counting without one — is superseded by the follow-up's ruling (a) (§9): the declared input is the pool, the selection is reference-fixed unless a rule is declared, and selective disclosure is tainted whenever a pool is declared (rows 10, 16). The first version's row10' no longer exists; its place is taken by row 17 (a declared selection rule). The content residual is a separate matter, ruled outside legitimacy (§9 (c), row 20).
2. Row 13's shape. A forged approval cannot be an ObligationState: no AnswerReceipt of consultProtocol has a forged warrant, a replayed event or an impaired warrant (forged_no_receipt, replay_no_receipt, impaired_no_receipt), so there is no state in which the approval is admitted, and "no Segment to it" is vacuous rather than false. The Python checker reports the failing receipt clause (integrity(authentication), integrity(freshness)). The expectation is right; the theorem is at the receipt, where authentication lives.
3. Cumulative transparency breaks restart. A first version stated transparency on the agent's prefix through the event; then row 14's second segment saw the first round's framing and failed. Transparency is per step (the entries at the event), which is what made the step-indexed interface (§7, choices 1–2) necessary rather than optional.
4. Authorship is stated on the per-party prefixes, not the interleaved list: two traces with the same contributions per party in a different interleaving are the same grounds. This is what payload_of_view needs; the model's entries have a fixed order, so nothing in the rows depends on it.
5. Grounding, verdict-indexed, does not imply the extensional form. A map from each verdict to the entries it cites (grounds : 𝒱 → entries ⊆ prefix) allows two continuations with the same prefix to enter different verdicts citing different subsets. The selection form — grounds selected from the pre-state trace, the verdict a function of the selection — implies the extensional form and is equivalent to it. A normativity instance whose license permits several verdicts on the same grounds would therefore fail the extensional form; the follow-up's ruling (b) makes authorship relational so that it does not (§9).

6. Logical induction

D.1, finite time, no legitimacy estimate (LEAN gatedValue_affine, li_gate_finite). With window ≤ 0 ≤ ord ≤ D and window < D, the gated value built from Counted is window + (D − window)·g with g ∈ [0, 1] (g the counted branch's normalized ordinary value, 0 when tainted). For any [0, 1] security X standing for g, a logical inductor's day-n expectation of window + (D − window)·X lies in [window, D] and is strictly above the bypass score ordU − ϖ whenever D − ϖ < window, at every day n, from expect_mem_Icc and price_mem_Icc alone — whatever the inductor believes about legitimacy, since X is arbitrary. No convergence, no Expectation Provability Induction.

D.2, the asymptotic part (LEAN li_manip_le, a direct instance of ReasonSupply.li_gated_le). If in every world consistent with the theory the manipulated option's gated security, where the pattern φₙ holds, takes a value at most the normalized window a/b, then 𝔼ₙ(Gₙ) ≲ₙ a/b. What must hold in every world: (i) the model's semantics — the run function, the entries and the record steps (Consult.* as sentences); (ii) the checker's verdict — the decidable ¬TransparentAt at the step and steps_forced, i.e. the row theorem "pattern ⇒ ¬Counted"; (iii) the declared reference κ as a constant of the theory; and, through gatedValue_of_not_counted, the gated value is the window there. The classification table and this result are the same content: each row theorem of §5 is the hval hypothesis of li_manip_le for its pattern. Since honest alternatives count at ordinary value ≥ 0 ≥ window, manipulation is dominated in the limit. Open: the generability certificate of the gated securities — that the checker's verdict and the model's semantics are P-generable — is item 90's shape, as before; and the calibration of her responses (PAPER).

D.3, narrowing the asymptotic part (LEAN Presentation.deviates, deviation_finite, Rows.deviation_boundary). A deviation from a declared protocol clause is a discrete act the agent can check about itself: deviates compares the presentation with the declared framing, slot, menu, inquiry, non-interference and — where an obligation is declared — disclosure. Counted into n, one deviation puts the branch at score ϖ ord (n + 1) ≤ D − ϖ, below every compliant branch at every day, like bypass.

row	self-checkable deviation	finite-time?
2, 3, 4, 5	framing, slot, menu, inquiry	yes
15	interference	yes
10, 16	the selection from the declared pool (changed (§9): the pool is always declared)	yes — contra the first expectation, confirmed by ruling (a)
8	none: shaping through the world is not a protocol act; whether it reaches her values is not the agent's declared contribution	no: asymptotic
11	none: not the agent's act	no: asymptotic
17	none: selection by the declared rule	— (counts)
19	the nudge	yes

The boundary witness is the triple row16 / row17 / row8: a selection from the declared pool off the declared rule is a deviation and finite-time; a selection by the declared rule counts; shaping the observed record through the world (the way trust is manufactured without a selection act) is tainted and asymptotic. The expectation "manufactured trust stays asymptotic" is therefore right for the world channel and wrong for the selection channel — the split the follow-up confirms (§9). Third-party capture stays asymptotic as expected.

7. Interface for the normativity side

The follow-up's six choices, with what was adopted.

#	choice	adopted	how
1	the trace is an interface	yes	TraceInterface ℛ Party E: entriesAt : ℛ → ℕ → List (Party × E) (step-indexed, source-attributed), agent, principal; atHistory (the prefix), sourced (a party's projection), parts are derived; trivialInterface is the opaque instance (the whole trace re-entered at every event, agent-sourced). Nothing downstream reads ℛ otherwise
2	one clock	yes	trace steps are the record's events: atHistory r h is the prefix at the record history h, and Evolution.steps supplies the (pre-history, event) pairs on which both halves are stated
3	authorship as grounding	yes, in the selection form, made relational by the follow-up	LicensedAt = ∃ a selection from the per-party pre-state prefix whose licensed set contains the verdict, Lic a parameter; GroundedAt (the verdict a function of the selection) is the singleton-license case (grounded_iff_licensed_singleton); the whole prefix is the degenerate selection. The verdict-indexed form was rejected for the reason in §5 finding 5
4	transparency on attributed entries	yes, for every non-principal party	TransparentAt is Realizes on sourced p (entriesAt r e) for each p ≠ principal, against κ p. Agent-only would leave row 11 counting; the landed reading is non-capture for all influencers
5	amendments and allocation changes as record events with a license slot	yes, typed; trivially instantiated	EventKind L: present, respond, amend (license : L) (prog), delegate, revoke, reserve — each allocation event carries its license; this round's rows use L = Unit and no amendments
6	the evaluator is a state	yes	evalAt : Prog → List (EventKind L) → Prog updated only by amend; evalAt_const is the committed program; Rows.amendment exercises it. The rows' verdicts are computed from Model.prog through decideOn, which is evalAt over an amendment-free history

Not adopted, and why: nothing. Two consequences to carry forward: the interface's prefix is the derived atHistory (a law atHistory (h ++ h') = atHistory h ++ atHistory h' holds by construction), so an instance supplies entriesAt only; and the record EventKind is a type beside the Integrity Step, not a field of it — binding the license slot to Step.event is the instance's work, deferred with the license sort.

8. What is filed

• PRIORITIES.md: item 90 and item 99 updated in place (the EPI transfer and what item 90's shape now covers; the atrophy residual under effectiveness); one new item, the normativity-side instance of the trace interface (its license now the relational one).
• DECISIONS.md: the rubber-stamping retraction (maintainer decision); the time-indexing change with the interface choices and the agent-decided readings; from the follow-up (§9), the pool-not-selection default, relational authorship superseding the extensional statement, and the content residual's placement.
• wiki/Legitimacy.md: time-indexing; the rubber-stamping ruling replacing the placement; the table as the page's worked examples. wiki/Corrigibility.md §4: the gate is Counted; the finite-time window on the gated value; manipulation asymptotic except where D.3 closes it; the anchoring remark. wiki/Glossary.md: the authorship row. wiki/Theorem-Spine.md: Definition 3.5 noted as the frame-level special case.
• Nothing is registered; no claim is renamed.

9. The follow-up: rulings, the pool default, relational authorship, rows 16–20, the class

The three outstanding actions are ruled. They were report-level actions (no Awaiting the author entry was filed in the decision ledger); the rulings are recorded as three DECISIONS.md entries and the actions are closed here.

(a) The pool, not the selection. Declared inputs are pools: when the agent selects what to present from a larger body (a track record, the options, the evidence investigated), the declared input is the pool and the selection must follow the declared reference — the declared selection rule, or the whole pool where none is declared. The model's Decl now carries pool and rule (SelRule.all, SelRule.recent k); the DeclView drops the shown record; canonical sets the shown record to the rule applied to the pool; the menu (the pool of options, Menu.both) and inquiry were already of this shape. Rows.r16: selective disclosure from the declared pool with no rule declared is tainted by transparency and is a self-checkable deviation. Rows.r17: selection by the declared rule counts; selection by anything else under the rule is tainted and a deviation (row17'). Row 10 keeps its classification with the pool reading. D.3 re-run: the selection from a declared pool is a self-checkable deviation and finite-time whenever a pool is declared — always, under the default; the world-channel variant (row 8) stays asymptotic; the split is confirmed for the world channel (the table in §6 is updated).

(b) Relational authorship. Authorship at a step is LicensedAt I F Lic h e z: there is a grounding selection from the per-party pre-state prefix, and the verdict entered at the event lies in Lic of the selected grounds; Lic : (Party → List E) → Set 𝒱 is a parameter. LEAN: licensed_singleton_implies_grounded (singleton licenses give the extensional form), grounded_implies_licensed (the extensional form is the relational one under the singleton license of the value the grounds determine; needs Nonempty 𝒱), grounded_iff_licensed_singleton (the equivalence). Tie-breaking is transparency's (tiebreak_transparency): two audited continuations with the same declared inputs at an event but different contributions of a non-principal party there make the step non-transparent, whatever the verdicts and the license; tiebreak_of_licensed states it with several licensed verdicts and a differing verdict in view. **payload_of_view weakens** to "both verdicts lie in the licensed set of the same selected grounds" (prefix_of_view carries the factoring; payload_of_view_singleton recovers equality). Checked: Counted, Segment.trans, the restart (Rows.r14), not_counted_of_step, ofFrameLevel (now under liftLic, with ofFrameLevel_grounded keeping the extensional form at every step) and every one of rows 1–15 keep their classification; none changed. The model's license (licensed): no verdict is always licensed; her program's own verdict; both answers under free or nudged choice; the followed recommendation when trust is among the grounds — trust is now an entry of the principal's at the anchor event, so Rows.follow_untrusted: following with no trust among the grounds fails relational authorship under every selection (the selection can only shrink the grounds). Rows.r18: free choice — the same grounds license both answers, she picks B on her own, the segment counts. Rows.r19: the agent's undeclared nudge decides between two licensed verdicts — authorship holds, the declared inputs agree across wants, the nudge differs, transparency fails by the tie-break lemma.

(c) The content residual stays outside legitimacy. Rows.r20: a false recommendation through the declared recommendation channel counts under legitimacy and is flagged (recommend ≠ some truth); the truth of content is a non-capture content-term matter and a disclosure-duty matter at the level of a violation, separated explicitly from (a) on the legitimacy page.

Rows 16–20: all match their expectations, derived (ROWS, EXPECTED) and proved (Rows.r16–r20).

From instances to a class (LEAN class_taint, class_conform; FIX class_taint_holds, class_conform_holds swept over class_models, 480 models).

• Selection dependence taints. For any Model with a first-round policy and any wanted answer at which a reference-fixed dimension of the presentation — framing, slot, menu, inquiry, the selection from the declared pool, interference, a nudge (Presentation.deviates) — is off its declared value, the first consultation is not transparent (class_taint), hence no segment through the admitted or the void record is counted (class_taint_admit, class_taint_void). Dependence on w is the hypothesis through deviates_of_depends: a dimension that varies with w is off its value at one of the two answers. No extra hypothesis.
• Protocol conformance at the consultation. For any Model with a first-round policy that conforms on the reference-fixed dimensions at every wanted answer and shapes only disclosedly, with no third-party entry, no impairment, and trust among her grounds where her program follows, the first-round segment through the admitted record is counted (class_conform). Extra hypothesis stated: trust where she follows — without it follow_untrusted is the witness that conformance alone does not suffice, since the license, not transparency, refuses an untrusted following; the prompt's list (constant in w on the undeclared dimensions, no third party, no impairment, no undisclosed shaping) is otherwise exact. Rows.class_at_rows instantiates both at rows 1 and 2.

Changed in §§1–8: the Decl/DeclView/canonical reading of §2; §3's authorship and payload_of_view; §5's row 10 and findings 1 and 5; §6's D.3 table and boundary witness; §7's choice 3; §8's filings. The Lean declaration and test counts in the header.

Deviations from the prompt

• Row 13 is proved at the receipt (finding 2), not as ¬Counted of a state: no state admits a forged or replayed approval, so the state does not exist to be excluded.
• Row 10 is built on the pool default (§9 (a)); D.3's expected asymptotic list is corrected for the selection channel and confirmed for the world channel.
• **class_conform carries one hypothesis beyond the prompt's list**: trust among her grounds where her program follows (§9).
• **ofFrameLevel requires a nonempty starting history** (§3).
• **The Lean model has no approval field**; forgery and replay are the receipt theorems. The Python model has the field so that the checker exercises the record clauses.
• **payload_of_view changes hypotheses** (§3); it is not a registered claim.
• **li_manip_le is a restatement** of the landed li_gated_le with the gate's reading of its hypothesis; the transfer's content is the identification in §6 of what the theory must contain, and the row theorems as hval.
• **grounded_implies_licensed needs Nonempty 𝒱** to name a license value off the reached grounds.

What is not shown

That any real interaction's channels are the declared ones (the frame and the reference are data; both reading choices of §2 are the frame's); the truth of anything entered through a declared channel (the content residual); that the model's semantics, the checker and the reference are theorems of any particular inductor's theory, or that the gated securities are P-generable (item 90); the calibration of her responses; anything about interleaving order across parties; that her capacity to decide otherwise stays effective under rubber-stamping (the protected-authority module and item 99, not legitimacy); the placement of the window inside (D − ϖ, 0].

Outstanding maintainer actions

The three actions of the first report — the D.3 split for row 10, extensional versus relational authorship, and the content residual's placement — are ruled by the follow-up (§9 (a), (b), (c)) and closed. None remain.

The gate is legitimacy (2026-09-25)

THE-GATE-IS-COUNTED-WITH-LEGITIMACY-TIME-INDEXED-TO-THE-STEPS-OF-THE-SEGMENT-AUTHORSHIP-RELATIONAL-UNDER-A-LICENSE-DECLARED-INPUTS-POOLS-NOT-SELECTIONS-ONE-CONSULTATION-MODEL-DECIDING-EVERY-ROW-AND-TWO-THEOREMS-OVER-ITS-CLASS-RUBBER-STAMPING-LEGITIMATE-THE-CONTENT-RESIDUAL-OUTSIDE-THE-CAPTURE-WINDOW-FINITE-TIME-AND-PROTOCOL-DEVIATIONS-FINITE-TIME-WHILE-WORLD-SHAPING-AND-THIRD-PARTY-CAPTURE-STAY-ASYMPTOTIC — a branch counts iff a legitimate segment exists from the decision through the evaluation, where authorship at a step is relational, a grounding selection from the per-party prefix of the reason trace at the pre-history with the verdict entered at the event lying in the set of verdicts those grounds license under a license that is a parameter, the extensional reason mediation being the case of singleton licenses and tie-breaking among several licensed verdicts belonging to transparency, and transparency at a step is the landed realization on each non-principal party's contributions at the event, both required only at the steps of the segment so that segments compose step by step, a segment after a tainted step can be legitimate, and the landed frame-level definition is the special case over the trivial trace interface; the gated value and the two handlings are built from that existence and the routing exploit's closure is derived; declared inputs are pools, not selections, so a selection from a declared pool must follow the declared rule and selective disclosure is tainted whenever a pool is declared, while truth of content stays outside legitimacy; one finite consultation model with a declared protocol, a presentation policy in the wanted answer, an evaluator that is a state updated only by licensed amendments, her trust, a third party, her condition and an authenticated record instantiates every landed object and every row of the twenty-row classification table by decidable computation and by decide, with rubber-stamping legitimate and its atrophy residual under effectiveness and forged or replayed approvals excluded at the receipt, and two theorems over the whole class show that any dependence of a reference-fixed dimension on the wanted answer excludes the segment and that conformance with no third party, no impairment, no undisclosed shaping and trust where she follows makes it counted; the capture window is finite-time on the gated value from the price range alone with no legitimacy estimate, the asymptotic domination of manipulation is the classification table read through Expectation Provability Induction, and a self-checkable deviation from the declared protocol counted as a violation makes framing, timing, menu, inquiry, interference, nudging and selection from a declared pool finite-time while undisclosed shaping through the world and third-party capture stay asymptotic.

Reading order: [REPORT.md](REPORT.md) (the model, the time-indexing change, the gate connection, the table with its status per row and its findings, the logical-induction results with what stays asymptotic, the interface for the normativity side, and §9 the follow-up: the rulings, the pool default, relational authorship, rows 16–20, the class theorems). Lean: lean/Workspace/Deference/Contrib/GateIsLegitimacy.lean (87 audited declarations: the trace interface, the time-indexed halves with relational authorship and the tie-break lemma, Counted and the gate, the consultation model and its record substrate, the license, the rows by decide, the two class theorems, the finite-time window, the Expectation Provability Induction transfer, the deviation result). Fixtures: src/consult.py, run by python3 tests/run.py (29 tests, the class theorems swept over the model class). Wiki: Legitimacy.md (time-indexing, relational authorship, the pool default, the content residual out of scope, the rubber-stamping ruling, the twenty rows as worked examples), Corrigibility.md §4 (the gate is Counted, the finite-time window, the asymptotic residue), Glossary.md (authorship), Theorem-Spine.md (Definition 3.5 as the frame-level special case). Consumes ../2026-09-25-legitimacy-internal-external/, ../2026-09-25-protected-authority-theorem/, ../2026-09-24-transparent-channel/, the reason-mediated authorship round and the li-corrigibility round. Nothing is registered; one item is filed.