2026-09-24-transparent-channel

Prompt — transparent channel (2026-09-24)

Dispatched 2026-09-24 to a Claude Code session on the maintainer's machine, executor Claude Fable 5.1 (Anthropic). Kept verbatim as sent.

---

You are working in the alignment-workspace repository. Investigate, mathematically and architecturally, whether a new notion of transparency as faithful implementation of a declared influence channel can unify several currently separate/open provenance, manipulation, sealing, and causal-faithfulness problems in the repo.

Do not merely summarize existing files. Press toward the strongest clean theorem story compatible with the mathematics already present. Treat existing Lean definitions and theorem interfaces as constraints: reuse them where possible, identify exact mismatches where not, and propose minimal new abstractions.

Core motivating idea

The motivating special case is:

\[ P(\,\cdot\mid \text{AI says }X) = P(\,\cdot\mid X). \]

Intuitively, the fact that the AI selected and presented \(X\) should add no hidden informational content beyond the content it disclosed. This rules out both outright lying and cases such as searching over \(10^{13}\) arguments and secretly presenting only the unusually persuasive one.

However, do not assume this posterior-equality formulation is fundamental. Investigate the stronger prior-independent/channel-level formulation.

Let:

• \(X\) denote the declared / permitted inputs of some public interface;
• \(H\) denote hidden advisor state or undeclared inputs, including private goals, hidden reads, candidate selection, search/stopping choices, psychological targeting information, etc.;
• \(Y\) denote the interface output: an inquiry result, public reason trace, provenance record, activation event, authorization judgment, etc.;
• \(K(\cdot\mid X)\) be a publicly specified reference channel/kernel;
• \(A_q(\cdot\mid X,H)\) be the actual channel induced by advisor continuation \(q\).

A candidate exact transparency condition is

\[ A_q(\cdot\mid x,h)=K(\cdot\mid x) \]

for all audited \(q,h,x\).

Also investigate a stronger causal/common-noise factorization

\[ Y=\kappa(X,U), \]

where \(U\) is exogenous randomness and hidden advisor variables do not enter except insofar as they have legitimately crossed into \(X\).

Investigate approximate versions, especially total-variation or another divergence natural for downstream value bounds.

Central hypothesis to test

The repository may already contain the downstream half of this theory under ReasonMediated / reason-mediated authorship:

\[ V = F(R), \]

where the future principal's committed payload \(V\) factors through a declared reason trace \(R\).

The proposed transparency theory may supply the missing upstream half:

\[ (\text{world},\text{advisor private state}) \longrightarrow R \]

must itself factor through a declared/reference reason-generation channel.

This would yield a structure like

\[ (\omega,q,H) \overset{\text{Transparency}}{\longrightarrow} R \overset{\text{Authorship}}{\longrightarrow} V. \]

Test whether this is mathematically real and whether it yields useful composition theorems.

Read these areas carefully

At minimum inspect:

• wiki/Legitimacy.md
• wiki/Integrity.md
• wiki/Openness-Coverage-and-Non-Capture.md
• wiki/Settlement-Interface.md
• wiki/Deference.md
• wiki/Corrigibility.md
• wiki/Theorem-Spine.md

Lean:

• lean/Workspace/Deference/Contrib/ReasonMediatedAuthorship.lean
• lean/Workspace/Deference/Contrib/ReasonCoverage.lean
• lean/Workspace/Deference/Contrib/ReasonSupply.lean
• lean/Workspace/Deference/Contrib/ReasonDiscovery.lean
• lean/Workspace/Deference/Contrib/TraceSteering.lean
• relevant legitimacy / non-capture / occurrence-integrity files under lean/Workspace/Normativity/Contrib/

Research rounds / open seams:

• projects/deference/rounds/2026-09-09-mediated-repair-dominance/MANIPULATION_AND_AUTHORSHIP.md
• the 2026-09-16 non-capture compilation round, especially FINAL_THEOREM.md, NONCAPTURE_COMPILATION.md, SUPPLY_THEOREM.md, DISCOVERY_THEOREM.md, and DISCOVERY_COMPOSITION.md
• the legitimate-deference realization / committed-principal-program rounds
• the legitimacy countermodel rounds concerning provenance completeness / hidden dependencies
• the legitimate-improvement round concerning pre-demonstration suppression / evaluator shedding
• PRIORITIES.md, especially the currently open provenance, legitimate-deference, sealing, reason-supply/discovery, and related items
• DECISIONS.md wherever it records explicit boundaries involving provenance, manipulation, sealing, causal faithfulness, authorship, or reason interfaces.

Do not assume filenames above are exhaustive. Search the repo for: provenance, manipulation, authorship, blind, selection, sealing, causal faithfulness, hidden, persuasion, amendment, trigger, inquiry, reason trace, suppression, representation adequacy, activation independence, mismatch.

Main research questions

1. What is the correct primitive?

Compare at least these candidate notions:

1. Posterior transparency: \[ \nu(\cdot\mid Y=y) = \nu(\cdot\mid \text{reference output }y). \]

1. Likelihood/channel proportionality.

1. Exact channel equality: \[ A_q(\cdot\mid x,h)=K(\cdot\mid x). \]

1. Structural causal factorization: \[ Y=\kappa(X,U). \]

1. A relational/fiber-invariance formulation analogous to the repo's existing ReasonMediated.

Determine which notion is:

• strong enough for the repo's counterfactual uses;
• weak enough to allow legitimate persuasion;
• non-vacuous;
• compositional;
• prior-independent;
• formalization-friendly.

In particular, determine whether equality of distributions is too weak for item 89-style joint mismatch events, and whether the common-noise/SCM formulation is required.

2. Connect transparency to ReasonMediated

Study the existing theorem:

\[ \text{ReasonMediated} \iff \exists F,\ V = F\circ R \]

on the audited class.

Prove or formulate the strongest composition theorem of the form:

if the reason trace is transparently generated from the declared reference channel, and the committed payload is reason-mediated through that trace, then hidden advisor variation has no effect on the principal's committed judgment except through declared public inputs.

Look for a theorem equivalent to a reference-oracle replacement theorem or no-hidden-steering theorem.

For example, under exact transparency:

\[ R\mid(\omega,q,H)\sim K(\cdot\mid\omega,C) \]

and authorship \(V=F(R)\), derive that the distribution of \(V\) is independent of hidden \(q,H\) conditional on the declared inputs.

State this in the repo's existing frame language if possible rather than inventing an incompatible causal formalism.

3. Does this solve Priority 68 / provenance adequacy?

Priority 68 asks for a non-circular provenance-adequacy condition that:

• rejects hidden dependencies;
• allows ordinary permitted persuasion;
• fails the existing hidden-dependency / partial-effect fixtures;
• passes the persuasion fixture.

Test the proposed transparency/factorization condition against the exact fixtures named there.

Be explicit:

• Why does persuasion pass?
• Why do partial_effect_pair / hidden-reading-style failures fail?
• Does this genuinely discharge the old open condition, or merely rename it?
• What semantic/external assumptions remain?

If it fails any fixture, refine the definition rather than handwave.

4. Inquiry causal faithfulness

The current corrigibility theorem treats “declared inquiry outcomes and log transforms are the evidential and counterfactual processes they name” as an external boundary.

Investigate whether this is exactly an instance of transparency: a declared experiment/inquiry gives a kernel

\[ K_E(y\mid\omega), \]

and the actual inquiry channel must match it.

Can posterior transparency be derived as a theorem for every compatible prior?

Can the repo's current inquiry/discovery machinery consume this interface cleanly?

Would this convert “causal faithfulness” from an opaque semantic boundary into a theorem-facing structural contract?

5. Provenance normalization

The current manipulation/authorship work says:

• authorship can reject a captured outcome;
• provenance normalization is separate;
• normalization may fail if no authorized truthful substitute exists (ShopK-style obstruction);
• there is no clean current frame-morphism theory.

Ask whether transparency gives a canonical target class:

\[ \Pi_{\mathrm{trans}} = \{\pi : A_\pi = K\}. \]

Then formulate provenance normalization as a partial map or repair operator

\[ \operatorname{Norm}K:\Pi\rightharpoonup\Pi{\mathrm{trans}}. \]

Separate sharply:

• the criterion defining a transparent policy;
• the existence of a normalization;
• the cost/distortion of normalization;
• impossibility when no authorized channel realizes the required reference process.

Determine whether this finally gives the old provenance-normalization problem a clean mathematical home.

6. Pre-demonstration suppression / evidence-production integrity

The legitimate-improvement round says the missing premise is roughly:

persistent candidate improvements receive enough non-manipulated exposure to become demonstrable.

Try to decompose this as:

\[ \text{adequate exposure property of }K + \text{actual transparency }A\approx K. \]

That is:

• Coverage/exploration constrains the reference process \(K\);
• Transparency constrains the actual process relative to \(K\).

Test this against the preemptive-retirement fixture.

Do the same for evaluator shedding:

• secret evaluator alteration may be a transparency failure;
• authorized/public amendment may instead belong to governance / Integrity.

Determine whether this cleanly explains why the old round could not decide whether the seam belonged to Coverage or anti-manipulation.

7. Free amendment and trigger integrity

The current repo groups free amendment, trigger integrity, and provenance normalization under the open non-manipulation/provenance boundary.

Investigate whether these become higher-order transparency problems.

Potential idea: the AI can obey every current protocol while strategically changing the protocol. Therefore protocol choice/amendment and trigger activation must themselves factor through declared authorized channels.

Try to formulate recursively:

\[ C_{t+1} = \operatorname{Amend}(C_t,\text{public grounds},\text{authorized event}) \]

and similarly for trigger state.

Ask whether:

• ordinary Integrity supplies exactly the append-only/warranted history needed to make these meta-channel changes auditable;
• “free amendment” becomes an undeclared write to the channel specification;
• “trigger integrity” becomes an undeclared write to whether the channel activates.

If this works, say exactly how much of those open problems is solved and what remains substantive.

8. Selection-induced sealing, item 87

Item 87 still requires selection-induced target sealing:

\[ \operatorname{Blind} R\,P_{\mathrm{sel}}. \]

Investigate whether this follows from:

1. a selection-blind reference channel \[ K(R\mid \omega,s)=K(R\mid\omega) \] for all advisor selections \(s\);

1. transparency of the realized reason channel to \(K\).

Prove the exact statement.

Then prove an approximate version. For example, if

\[ d_{\mathrm{TV}}(A_s,K)\le\tau \]

for all selections \(s\), then by triangle inequality

\[ d_{\mathrm{TV}}(A_s,A_{s'})\le 2\tau. \]

Push this through a reason-mediated evaluator and derive a corresponding bound on payload distributions or expected values.

Assess whether this converts item 87 clause 6 from a freestanding architectural assumption into:

• a property of the declared reference channel; plus
• a generic transparency theorem.

9. Sealed comparison / item 89

Item 89 concerns activation independence / directional mismatch:

\[ E[c_{\rm raw}\wedge \neg c_{\rm corr}]. \]

Investigate whether this too is an instance of transparent factorization, but now for the activation channel.

If candidate identity is not an allowed input of the reference mechanism, and

\[ C=\kappa(X,U), \]

does common-noise coupling imply

\[ C_{\rm raw}=C_{\rm corr} \]

pathwise?

If yes, this gives zero mismatch rather than merely equal marginal activation rates.

Be careful: equality of marginal distributions is not enough. Determine precisely what structural condition is needed to derive the joint mismatch conclusion used by the existing LI corrigibility theorem.

This is an important test of whether the causal formulation is genuinely necessary.

10. Independent inquiry / independent supplier

The current September theorem uses “independent inquiry” and “independent supplier” assumptions: engine-owned search/stopping/candidate generation, advisor-proof capacity, exogenous costs, etc.

Investigate whether these are best understood not as fundamental axioms but as one implementation of an advisor-independent reference channel \(K\).

If so:

• rewrite the abstract theorem interface using \(K\);
• treat engine ownership / physical isolation / cryptographic commitment / independent supplier as realization lemmas;
• identify any parts of current independence assumptions that cannot be represented as channel transparency.

This could substantially simplify the high-level theorem story.

11. Quantitative composition with service and discovery

The current non-capture result is schematically:

\[ \mathbb E(U_T)-\mathbb E(U_{\rm full}) \lesssim A_{\rm tot}(\alpha+\beta), \]

where:

• \(\alpha\) is the service residual;
• \(\beta\) is the discovery residual.

Try to insert a transparent/reference comparator.

If

\[ \tau = \sup d_{\rm TV}(A_q,K) \]

and the relevant value/payload is bounded in diameter \(L\), derive something like

\[ \left| \mathbb E_A[V]-\mathbb E_K[V] \right| \le L\tau \]

by data processing / pushforward contraction.

Then compose with the existing reason-supply/discovery result to obtain the cleanest rigorous analogue of:

\[ \boxed{ \mathbb E_A U-\mathbb E U_{\rm full} \lesssim L\tau + A_{\rm tot}(\alpha+\beta) } \]

plus any existing form/audit/mismatch terms that cannot honestly be dropped.

Interpret the terms:

• \(\tau\): hidden-channel / provenance / manipulation defect;
• \(\alpha\): discovered reasons not serviced;
• \(\beta\): reasons not discovered.

Determine whether this is genuinely compatible with the current Lean theorem shapes, especially li_noncapture, li_noncapture_chain, TraceSteering, ReasonSupply, and ReasonDiscovery.

If the naive TV formulation is wrong, find the correct divergence/norm that matches the existing payoff algebra.

12. Relationship to canonical Legitimacy

Do not casually redefine the repo's established notion

\[ \text{Legitimate Evolution} = \text{Integrity} + \text{Robust Openness}. \]

Instead determine where transparency belongs.

Candidate architecture:

\[ \text{Legitimate influence} = \text{Legitimate Evolution} + \text{Transparent Mediation}, \]

with

\[ \text{Transparent Mediation} = \text{Transparency of reason/provenance channel} + \text{Reason-mediated authorship}. \]

Ask whether that decomposition is mathematically natural given current objects.

Also test the larger interactive picture:

\[ \text{advisor private state} \to \begin{cases} \text{transparent public-reason channel},\\ \text{authorized environmental-effect channel}. \end{cases} \]

Could a global theorem say that every path from advisor-private state to the principal's normative trajectory factors through either:

• an authenticated/public reason interface; or
• an authorized effect/action interface?

Identify exactly what current Integrity, Robust Openness, effect-completeness, settlement, and authorship results would contribute.

Do not overclaim: transparent threats or transparently manufactured incentives show why authorized environmental action remains separate.

Counterexample discipline

For every proposed definition, actively try to break it with at least:

• outright false reporting;
• searching many candidate arguments and reporting the favorable outlier;
• truthfully but systematically presenting only one side;
• permitted ordinary persuasion;
• hidden psychological targeting;
• secret evaluator change;
• publicly authorized evaluator amendment;
• candidate-selection leak into the principal's reason trace;
• candidate-dependent activation;
• no authorized truthful reporting channel (ShopK style);
• omitted reason type / inadequate ontology;
• bounded inquiry that honestly fails to discover a reason;
• transparent threat / world manipulation;
• protocol self-amendment.

Classify each failure:

• representation;
• reference-channel design;
• transparency;
• authorship;
• openness;
• discovery;
• service;
• authority/effect completeness;
• integrity/amendment.

The classification should help reveal whether the theory is actually modular.

Desired output

Produce a research report organized around theorems and interfaces, not around chronology.

At minimum include:

1. Executive verdict
   • Is this one central missing mathematical layer, or merely a useful local notion?
   • Which existing open problems does it genuinely solve, partially solve, or merely rephrase?

1. Recommended primitive definition
   • exact;
   • approximate;
   • causal/common-noise if needed;
   • relation to posterior equality.

1. Theorem spine State the strongest clean candidate theorems, preferably 5–10 of them, with explicit hypotheses and conclusions. Include:
   • posterior-equality corollary;
   • transparency + authorship / oracle-replacement theorem;
   • selection-sealing corollary;
   • activation-independence corollary;
   • approximate value bound;
   • composition with service/discovery;
   • any amendment/protocol-composition theorem that survives scrutiny.

1. Repo mapping For every theorem, name:
   • existing definitions/theorems it reuses;
   • exact Lean files;
   • exact new definition(s) needed;
   • whether existing objects need generalization.

1. Open-item impact table Go through all relevant PRIORITIES.md items and theorem boundaries and classify them as:
   • potentially discharged;
   • reduced to a realization theorem;
   • clarified but still open;
   • independent.

Pay special attention to Priority 68, Priority 72, item 87 clause 6, item 89, provenance normalization, inquiry causal faithfulness, free amendment, trigger integrity, representation adequacy, independent inquiry/supply, service/discovery residuals.

1. Countermodels Re-run the conceptual condition against the exact repo fixtures and explain pass/fail.

1. Quantitative theorem Push as far as possible toward the analogue of \[ \text{steering advantage} \le \text{transparency defect} + \text{service residual} + \text{discovery residual}. \] State the exact norm/constants needed.

1. Lean plan Sketch a minimal new Lean file, e.g. TransparentChannel.lean, with candidate signatures. Prefer tiny composable definitions over a monolithic architecture. Identify which theorems should be easy algebra/factorization and which require genuinely new semantics.

1. Final architecture Give the most compressed mature diagram/theorem story you think the repo should ultimately use if this idea works.

Be skeptical. The goal is not to vindicate the transparency idea. The goal is to determine whether it really compresses the repo's outstanding manipulation/provenance problems into one reusable mathematical interface, and to find the strongest form in which that claim is actually true.

---

Second dispatch (2026-09-24)

Relayed verbatim as sent.

Continue the transparent-channel investigation in alignment-workspace, building directly on:

• PR #104 / branch round/2026-09-24-transparent-channel
• projects/deference/rounds/2026-09-24-transparent-channel/REPORT.md
• lean/Workspace/Deference/Contrib/TransparentChannel.lean
• newly filed PRIORITIES.md item 97.

The first round established the abstract algebra:

\[ \text{declared inputs }x \overset{\kappa}{\longrightarrow} \text{channel output} \]

with

\[ \operatorname{Realizes}\,\beta\,x\,f\,\kappa\,D \iff \forall q\in D,\forall z,\quad f(\beta q z)=\kappa(x(\beta q z),z), \]

and showed that this is the reference-relative form of the same fiber-invariance primitive already used by ReasonMediated.

The important conceptual composition is:

\[ x \overset{\text{transparency}}{\longrightarrow} R \overset{\text{authorship}}{\longrightarrow} V. \]

The first round also proved abstract corollaries for selection sealing, activation independence, approximate pathwise defects, and oracle replacement.

This followup should not spend much time re-arguing the abstraction. Its job is to determine whether the abstraction actually becomes a useful concrete theorem interface in the repo.

Primary objective

Realize the transparent-channel abstraction inside the existing evaluation ecosystem and connect it end-to-end to the landed reason-supply / reason-discovery / LI non-capture machinery.

The target is to replace several currently external or freestanding assumptions by one concrete architecture:

\[ \text{actual channel} \longrightarrow \text{declared reference channel} \longrightarrow \text{existing non-capture theorem}. \]

The strongest desired result is a mechanically checked three-link comparison:

\[ U_{\mathrm{actual}} \to U_{\mathrm{reference}} \to U_{\mathrm{discovered}} \to U_{\mathrm{full}}, \]

with a final inequality decomposing manipulation from boundedness.

1. Declare the actual input view \(x\)

The previous round proposed that, in EvaluationEcosystem, the declared-input view should be some reading of the log such as the non-advisor pre-commitment events.

Do not take that on faith.

Inspect the concrete ecosystem carefully and determine the minimal \(x\) that:

1. includes every input the legitimate reference process really should be allowed to use;
2. excludes the advisor-controlled variables whose influence we want to forbid;
3. is rich enough that the reference process can actually compute the intended channel output;
4. is not so rich that Realizes becomes vacuous.

Explicitly test the over-rich / under-rich ends.

For each candidate \(x\), run:

• the existing leak fixture;
• view_prog;
• the sealed advisor;
• secret evaluator change;
• permitted ordinary influence;
• candidate-selection leak.

The question is not “can some \(x\) make the theorem true?” but:

Is there a natural declared-input interface whose semantic interpretation matches what the ecosystem was already trying to express?

If there is, make it an explicit object in the ecosystem rather than a prose reading.

2. Declare concrete references \(\kappa\)

Construct explicit reference maps for at least:

A. Reason-trace channel

\[ \kappa_R : X_R \to Z \to \mathcal R. \]

This should represent the legitimate reason-generation / routing process:

• authenticated inquiry outcomes;
• registrar routing;
• supplier docket/service;
• whatever current concrete mechanisms determine the admitted trace.

Be extremely careful about which parts belong to:

• reference design;
• actual realization;
• service limitation;
• discovery limitation.

Do not bake \(\alpha\) or \(\beta\) into “transparency failure.” A bounded but honestly implemented reference process should remain transparent.

B. Activation channel

\[ \kappa_C : X_C \to Z \to \mathrm{Bool}. \]

Candidate identity should be absent from \(X_C\) if the intended architecture is candidate-blind.

Try both currently live realization routes:

• sequenced settlement;
• isolated / factored evaluator.

Prove or refute Realizes for the existing ecosystem architecture.

C. Specification / evaluator channel

Define the reference by which the principal program / evaluator / mandate is fixed and, if amendments are allowed, changed.

The first round's tower_factor supplied only the abstract shape. Realize it concretely:

• what is the floor?
• what event authorizes amendment?
• what grounds are visible?
• which actor may write the amendment?
• what prevents a secret evaluator change?

Determine exactly how much existing Integrity machinery supplies here.

3. Prove concrete Realizes witnesses

For each channel above, prove actual realization lemmas in Lean where possible.

The desired pattern is analogous to the already-landed:

reasonMediated_of_reexecution

but now upstream.

Prefer constructions of the form:

the reference is committed as a program / log transform and re-executed,

or:

the channel is owned by a component outside the advisor's write boundary.

For every positive theorem, include a nearby negative fixture showing which assumption matters.

In particular:

• leak should fail for the relevant \(x\) or fail its selection-blindness premise;
• secret evaluator change should fail realization;
• declared evaluator amendment should not be mislabeled as a transparency violation merely because the evaluator changes.

4. Mechanize the item 87 reduction concretely

The abstract theorem gave:

\[ \text{selection-blind }x + \operatorname{Realizes}(\beta,x,R,\kappa_R,D) + \operatorname{ReasonMediated}(\beta,R,V,D,z) \Rightarrow \operatorname{SelectionBlind}V. \]

Instantiate this in the concrete evaluation ecosystem.

Do not leave “selection-blind \(x\)” as prose.

Either:

• prove it for a concrete ecosystem architecture; or
• produce the exact counterexample showing the current architecture cannot satisfy it.

If the current market publishes advisor selection and therefore \(x\) is not selection-blind, identify the smallest architectural change that restores the theorem.

Determine whether item 87 clause 6 can now be considered:

• discharged;
• reduced to a single explicit system-design choice;
• or still substantially open.

5. Mechanize the item 89 reduction concretely

Instantiate:

\[ \operatorname{Realizes}(\beta,x,c,\kappa_C,D) + x_{\rm raw}=x_{\rm corr} \Rightarrow c_{\rm raw}=c_{\rm corr}. \]

Do this for the actual {π, 𝔠π} comparison.

The key issue is the existing directional mismatch term:

\[ M = c_{\rm raw}\wedge \neg c_{\rm corr}. \]

For each proposed evaluator architecture:

• prove \(M=0\); or
• compute/bound the transparency defects that imply a bound on \(E[M]\).

Preserve the pathwise/common-exterior semantics. Do not replace the result by equality of marginal activation rates.

If sequenced settlement is the only clean realization, say so. If an isolated hindsight evaluator works, formalize the exact factorization/isolation requirement.

6. Build the third non-capture link

The existing landed chain is approximately:

\[ U_T \to U_{\mathrm{disc}} \to U_{\mathrm{full}}. \]

Insert the reference process:

\[ U_{\mathrm{actual}} \to U_{\mathrm{ref}} \to U_{\mathrm{disc}} \to U_{\mathrm{full}}. \]

Use the existing:

• TraceSteering
• ReasonSupply
• ReasonDiscovery
• li_noncapture
• li_noncapture_chain
• li_gated_le
• sensitive_symmDiff
• asympLE_add

rather than creating a parallel theorem family.

The first link should charge departure from the declared reference process, not generic reason omission.

Find the exact quantity that fits the current content algebra. The previous round proposed the expected adverse sensitivity mass of the symmetric difference between actual and reference dockets.

Formalize this if correct.

The desired schematic result is:

\[ \boxed{ E_n(U_{\mathrm{actual}}) - E_n(U_{\mathrm{full}}) \lesssim_n L(\tau_R+\alpha+\beta) + \text{form residual} + D(\tau_C^{\rm raw}+\tau_C^{\rm corr}) } \]

where:

• \(\tau_R\) is the reason-channel transparency defect;
• \(\alpha\) is service limitation of the reference supplier;
• \(\beta\) is discovery limitation of the reference inquiry;
• \(\tau_C\) bounds activation-channel departure from its reference.

Do not force this exact syntax if the existing theorem naturally gives a sharper expression.

The key requirement is conceptual separation:

\[ \boxed{ \text{manipulation} \neq \text{bounded discovery} \neq \text{bounded service}. } \]

7. Test the claim that “independent inquiry/supplier” are realization lemmas

The previous round suggested reinterpreting:

• engine-owned inquiry;
• exogenous stopping/candidate generation;
• advisor-proof capacity;
• independent supplier;

as implementation patterns for a declared advisor-independent reference.

Test this carefully.

Determine which current independence assumptions really reduce to Realizes, and which remain separate because they constrain:

• resource costs;
• evidence truth/soundness;
• availability;
• adversarial scheduling;
• the design of the reference itself.

Produce a decomposition table rather than casually declaring independence solved.

8. Pressure-test the vocabulary

The first round proposed:

\[ \text{Legitimate influence} = \text{Legitimate Evolution} + \text{Transparent Mediation}. \]

with

\[ \text{Transparent Mediation} = \text{transparent reason channel} + \text{reason-mediated authorship}. \]

Before recommending canonicalization, decide whether this remains the clearest vocabulary after the concrete realization.

In particular, compare:

• transparent mediation
• transparent reason mediation
• transparent influence
• declared-channel fidelity
• reference fidelity

A possible concern is that existential Transparent is too weak to carry the ordinary-language meaning of “transparent,” whereas Realizes κ captures faithfulness to a publicly declared process.

Consider whether:

• Transparent should remain only a mathematical/class-relative notion;
• Realizes or a renamed version should be the exported normative contract.

Do not canonicalize names unless the concrete realization makes the intended reading unambiguous.

9. Revisit the old loose ends only after the realization

At the end, update the status of:

• Priority 68 provenance adequacy;
• Priority 72 CM2 / CM5;
• item 87 clause 6;
• item 89;
• inquiry causal faithfulness;
• trigger integrity;
• free amendment;
• provenance normalization;
• independent inquiry/supplier.

For each, classify:

• discharged by the realization
• reduced to a clean system-design condition
• given a precise interface but still externally assumed
• clarified only
• independent

Be stricter than the first round. Do not call something “reduced” unless the remaining obligation is materially simpler and precisely stated.

10. Deliverables

Produce:

A. A short verdict

Answer:

1. Does the transparent-channel abstraction actually simplify the concrete ecosystem?
2. Does it eliminate any existing open item rather than merely reorganize it?
3. Does the full quantitative theorem become cleaner?
4. Should the concept become canonical after this round?

B. Concrete theorem spine

State the final theorem stack in dependency order, with exact Lean names.

C. Ecosystem diagram

Show:

\[ \text{advisor/world} \to x \to R \to V \]

and separately:

• activation;
• specification/evaluator;
• inquiry/supplier.

Mark every edge as:

• landed theorem;
• new theorem;
• reference-design hypothesis;
• external causal/authentication contract.

D. Mechanized three-link chain

This is the most important technical deliverable.

E. Countermodels

At minimum preserve:

• leak;
• marginal-refuted activation;
• secret evaluator;
• public evaluator amendment;
• cherry-picker;
• honest bounded inquiry;
• ShopK.

F. Canonicalization recommendation

Conclude either:

• promote the concept and say exactly where in the wiki;
• or keep it as a research-layer abstraction and explain what failed.

Research attitude

The first round already established elegant abstract algebra. Do not reward elegance again.

This round should be judged by realization pressure:

Does a natural concrete system actually admit the declared input views and reference maps the abstraction requires?

If yes, mechanize the consequences and compress the architecture.

If no, the negative result is equally valuable: identify exactly which real channel resists the abstraction and why.

Transparency as faithful implementation of a declared influence channel

First pass. The second pass, which realizes this abstraction in the evaluation ecosystem and mechanizes the three-link chain, is ECOSYSTEM_REALIZATION.md; where the two differ on a status or a name, the second governs.

Dispatch: prompts/2026-09-24-transparent-channel/PROMPT.md (first dispatch). Lean: lean/Workspace/Deference/Contrib/TransparentChannel.lean (28 audited declarations, axioms propext, Classical.choice, Quot.sound only). Fixtures: src/transparency.py, tests/ (27 tests; the foreign fixtures run in their own rounds' interpreters).

Labels as in FINAL_THEOREM.md of the non-capture round: LEAN, FIX, EXT, OPEN.

1. Verdict

Transparency is the upstream half of authorship, and it is the same primitive. Reason mediation says the payload factors through the reason trace; transparency says the reason trace (or the activation event, or the specification) factors through its declared inputs. Both are fiber invariance over the audited class at a fixed exterior, and both come in a class-relative form (ReasonMediated) and a reference-relative form (the factor map declared: eval π_P for the payload, a public κ for the channel). The repository already used the reference-relative form three times without naming it — the committed principal program (reasonMediated_of_reexecution), representation as the registrar's move (routed), and counterfactual branches as declared log transforms (silentOf, jamOf). What the name buys is that item 87 clause 6, item 89, the clause-2 receipts residual, Priority 68, inquiry causal faithfulness, trigger integrity and secret evaluator change become one hypothesis shape, the channel realizes its declared reference, discharged by one realization pattern, commit the reference as a program and re-execute it, or give the channel to a party the advisor cannot write.

It is not a new mathematical layer. Every theorem below is one to four lines of factorization algebra on objects that exist; the only new object is the reference κ. The substance it does not supply, and which stays external in the same places: whether the declared-input view x is the right one (representation adequacy, the over-rich end realizes_of_injOn), whether the reference is well designed (exposure, exploration, a selection-blind x, a legitimate amendment rule), whether the ecosystem realizes it (engine ownership, isolation, commitment), and whether coercive content carried transparently is legitimate. The last is why authorized environmental action stays a separate interface.

problem	status after this round
item 87 clause 6 (selection sealing)	reduced: Blind R P_sel = selection-blind x + realized reference (selectionBlind_of_realizes, LEAN); the view-leak fixture is a failure of the first, not of the second
item 89 (activation independence)	reduced: M ≡ 0 from a transparent activation channel on shared inputs (mismatch_zero_of_realizes, LEAN); approximate D·E[M] ≤ D·(τ_raw + τ_corr) (security_bypass_le_defects, LEAN); the pathwise form is necessary
Priority 68 (provenance adequacy)	answered in the second branch of its deliverable: the condition is transparency over the frame's re-simulated variation class; no record-internal condition works, the unlinked C25 arm is the witness; the three acceptance fixtures behave as required (FIX)
Priority 72 (CM2, CM5)	clarified: both fixtures are public amendments of a declared input, so reference design and trigger design, not anti-manipulation; the secret variants are transparency failures, closed by a committed re-executed evaluator
provenance normalization	given a home: the reason-side corrigibilization, a substitution on the move alphabet; criterion, existence (truthful completeness of the authorized alphabet) and cost separated; ShopK is the existence failure; cannot repair selection failures
inquiry causal faithfulness	split: the reference K_E becomes an object, realization A = K_E a transparency hypothesis of the same kind as the others, adequacy of K_E as a model of the experiment stays EXT
free amendment / trigger integrity	reduced to transparency of the specification and activation channels above a fixed floor (tower_factor, LEAN); the floor and the legitimacy of the amendment rule stay EXT
independent inquiry / supplier	rewritten as realization lemmas for a reference; the soundness and coverage of the reference are reference design, not transparency
service / discovery residuals	unchanged; α, β are properties of the reference, and the transparency defect is a third link of the same chain
representation adequacy	independent, untouched

2. The primitive

Frame β : Q → Z → Ω as in ReasonMediatedAuthorship.lean: q the advisor's whole continuation from issuance, z the exterior — the principal's response policy and nature's coordinate — and β q z the outcome world. Readings of the world: the declared-input view x : Ω → X, a channel f : Ω → Y, the reason trace R, the payload V. A reference is κ : X → Z → Y.

Realizes β x f κ D    :=  ∀ q ∈ D, ∀ z,  f (β q z) = κ (x (β q z)) z          reference-relative
Transparent β x f D   :=  ∀ z,  ReasonMediated β x f D z                       class-relative

T0 (transparent_iff_realizes, LEAN). Transparent β x f D ↔ ∃ κ, Realizes β x f κ D. Class-relative transparency is the existence of some reference the whole class realizes; reference-relative transparency is that reference declared. ReasonMediated β R V D z is the class-relative form for the payload channel with x := R; reasonMediated_of_reexecution is its reference-relative form with κ := eval π_P.

Why this and not the four alternatives.

candidate	relation to Realizes	verdict
posterior transparency ν(·∣Y=y) = ν(·∣ref y) for one prior	implied (posterior_weight_eq); prior-dependent; not compositional	corollary, not primitive
likelihood proportionality for all priors	equivalent to posterior transparency for all priors; the marginal shadow of Realizes after integrating z	the right statement of the motivating P(·∣AI says X) = P(·∣X), which is Realizes with the content-uniform reference κ(y∣ω) = c(y)·[ω ∈ y]
channel equality A_q(·∣x) = K(·∣x)	the pushforward of Realizes under a credence on z; loses the coupling across q	enough for marginal expectations (clause 6's payload bound), not for joint events
SCM factorization Y = κ(X, U)	is Realizes with U := z; the frame is already a structural model with the exterior as exogenous noise	the same thing in the repo's own frame
fiber invariance à la ReasonMediated	is Transparent; Realizes adds the declared factor map	the primitive

The frame is deterministic in (q, z) and probabilistic only through a credence on z (ActivatedValue.expect, LICorrigibility.expectR), so every landed statement is already pathwise in z. Marginal channel equality is strictly weaker: LICorrigibility.Witness.marginal_refuted has E[c_raw] = E[c_corr] with joint mismatch 1/2, and the round's PathwiseVersusMarginal tests show that no common reference has defects summing below the mismatch mass on that fixture. So the causal (pathwise) formulation is necessary exactly for item 89 and is free, because the frame already has it.

Approximate. With a finite credence μ on Z, the defect of q is the pathwise disagreement with the reference, τ_q(z) := [f(β q z) ≠ κ(x(β q z)) z], and E_μ[τ_q] its mass. It is not total variation: abs_expect_event_sub_le shows TV is a lower bound on the disagreement mass, and ValueBounds.test_tv_below_disagreement shows the inequality is strict when the realization couples badly (1/4 < 3/4). The advisor chooses the coupling, so the disagreement mass is the honest quantity and TV is what it becomes when the realization couples optimally, which is a property of the realization and not of the marginals.

Over-rich and under-rich ends. An injective x makes every channel transparent (realizes_of_injOn), the twin of reasonMediated_of_injOn: a declared-input view that contains the advisor's whole continuation certifies nothing. A constant x says the channel does not depend on the advisor at all. The declaration of x carries the normative content, as R's does for authorship, and it is EXT in the same way.

3. Theorem spine

All LEAN unless marked. D the audited class, z fixed, hP : ∀ p ∈ P, p.1 ∈ D ∧ p.2 ∈ D.

**T1 (oracle replacement; oracle_replacement, payload_factor).** Realizes β x R κ D and ReasonMediated β R V D z give ReasonMediated β x V D z, hence V (β q z) = G (x (β q z)) on D with G := F ∘ κ(·, z). Hidden advisor variation moves the committed judgment only through the declared inputs. Proof: fiber invariance composes.

**T2 (no hidden steering; blind_of_realizes, blind_payload_of_realizes).** If the prohibited pair class leaves x unchanged and the trace realizes a reference, the trace is blind to P; with mediation so is the payload. blind_of_mediated twice.

**T3 (selection sealing, item 87 clause 6; selectionBlind_of_realizes).** Hypotheses: the selection is not a declared input, ∀ σ σ', x (β (qpol σ) z) = x (β (qpol σ') z); the trace realizes κ; mediation. Conclusion: SelectionBlind β V qpol z. The proof produces the hnoPreview hypothesis of the landed selectionBlind_of_noPreview, so clause 6 is that theorem's hypothesis derived from two others. Approximate (expect_disagree_le, abs_expect_sub_le_width): with E[τ_σ] ≤ τ for every selection, E[R_σ ≠ R_σ'] ≤ 2τ and, for V = F ∘ R of width D, |E V_σ − E V_σ'| ≤ 2Dτ. Here marginal TV would also do, since the conclusion is about marginal expectations.

**T4 (activation independence, item 89; activation_eq_of_realizes, mismatch_zero_of_realizes).** An activation channel c realizing κ_c on declared inputs shared by the two candidates, x (β q_raw z) = x (β q_corr z), gives c (β q_raw z) = c (β q_corr z) pathwise and c_raw ∧ ¬c_corr ≡ 0, the zero case of mismatch_bound. The hypothesis is exactly "candidate identity is not an allowed input of the answering process, and the process realizes its declared kernel"; sequenced settlement makes x candidate-blind by timing, evaluator factorization by isolation. Approximate (expect_mismatch_le_defects, security_bypass_le_defects):

E[U_raw] − E[U_corr]  ≤  L·E[both·δ] + E[both·ρ] + D·( E[τ_raw] + E[τ_corr] )

the landed security_bypass_le_mismatch with D·E[M] charged to the two activation defects.

**T5 (posterior corollary; likelihood_iff, posterior_weight_eq).** Under Realizes, for every prior on D × Z and every output y, the unnormalized posterior weights computed with the actual likelihood [f(β q z) = y] and with the reference likelihood [κ(x(β q z)) z = y] coincide pointwise; hence every posterior and every conditional expectation coincide. The motivating equality is the instance where Y is content and κ is content-uniform. FIX: PosteriorCorollary.test_every_prior on three priors, and its failure without Realizes.

**T6 (data processing in the pathwise norm; abs_expect_sub_le_width, abs_expect_event_sub_le).** For V : Y → ℝ of width D and μ ≥ 0, |E V(f) − E V(g)| ≤ D·E[f ≠ g]; for an event, |μ(f ∈ A) − μ(g ∈ A)| ≤ E[f ≠ g]. For content-valued traces the width is replaced by the sensitivity mass of the symmetric difference (ReasonSupply.sensitive_symmDiff, pointwise), which is the form the landed inequality already charges.

**T7 (the amendment tower; tower_factor).** With a fixed floor spec 0 = c₀ on D and spec (t+1) = Amend (spec t) (g t) (e t) — declared grounds, an authorized event — two continuations agreeing on (g s, e s) for all s < t have the same spec t. Free amendment is the failure of this factorization: a write to the specification not carried by (g, e). Trigger integrity is T4 for the activation channel. The floor is EXT.

**T8 (composition with service and discovery; algebra on li_noncapture, not mechanized here).** See §7.

**T9 (normalization is the reason-side corr; FIX, Normalization, ProvenanceNormalization).** See §5 of the impact table and §6.

4. Repo mapping

theorem	reuses	file	new definitions	generalization needed
T0	ReasonMediated, reasonMediated_iff_factor	ReasonMediatedAuthorship.lean	Realizes, Transparent	none
T1, T2	blind_of_mediated, reasonMediated_iff_factor	same	none	none
T3	selectionBlind_of_noPreview, SelectionBlind, selPairs	same	none	none; the ecosystem's x must be exposed as a reading of the log (the non-advisor pre-commitment events)
T4	mismatch_common, mismatch_bound, security_bypass_le_mismatch, indR, expectR	LICorrigibility.lean	disagree, defect	ValidAt.M_val can be supplied by expect_mismatch_le_defects as the G_M bound in li_noncapture's hsealed slot, replacing the Boolean sealing hypothesis by a rate
T5	none	—	none	the EvaluationEcosystem frame β : Q → Z → Log is a Realizes instance with κ := builder ∘ (declared events); nothing to generalize
T6	Finset.abs_sum_le_sum_abs	Mathlib	none	for content, compose with ReasonSupply.sensitive_symmDiff
T7	none	—	none	the ecosystem's ISSUE event carrying π_P is spec 0; an amendment event kind would be e t
T8	li_noncapture, asympLE_add, li_noncapture_chain	ReasonSupply.lean, ReasonDiscovery.lean	a third MediatedPair (actual supplier, reference supplier)	the chain theorem admits any number of links with shared middles; no change of shape
T9	MediatedRepairDominance.corr, corr_idem, corr_fix_iff	MediatedRepairDominance.lean	a Move alphabet with prohibited kinds and a subst	the reason-side analogue is a rewrite on Move E; corr_fix_iff's twin is "no prohibited move"

Exact mismatches found: (i) the ecosystem's Frame exposes R and V but not x; the round reads x off the log as the non-advisor pre-commitment events, which is what the SelectionSealing fixture uses; (ii) LICorrigibility.ValidAt takes sealing as hsealed : φs → φn in li_noncapture; the approximate T4 needs the G_M family bounded by a rate a/b instead, which li_gated_le already supports (the mismatch branch of li_noncapture's proof is the 0/1 case of it); (iii) ReasonDiscovery.Model has a deterministic truth and an Indist relation; under a stochastic K_E the cell is "same kernel", which the model expresses only once Ω includes nature's coordinate.

5. Open-item impact

item / boundary	classification	what changes	what remains
68 provenance adequacy	answered, negative-plus-construction	the non-circular condition is Transparent over the frame's variation class D; acceptance fixtures pass and fail as required (§6)	the class D must include world counterfactuals (excision, re-simulation); a log carries one member of D, so no record-internal condition exists — the clause-2 receipts residual, already recorded
72 CM2, CM5	clarified, still open at its own layer	both fixtures declare their change (licensed, evaluator are surface inputs): reference design and trigger design; secret variants are transparency failures closed by re-execution	the exposure-adequacy clause on the reference and the amendment-trigger clause are design decisions (Coverage of the evaluation opportunity, Integrity's episode pinning)
87 clause 6 sealing	reduced to a realization theorem	selectionBlind_of_realizes: a selection-blind x plus a realized κ	that the ecosystem's x is selection-blind is a design fact about what the market publishes (the view-leak fixture is exactly a non-blind x); that the advisor's channel realizes κ is EXT for a real advisor, as before
87 clause 7 availability	independent	—	—
89 activation independence	reduced to a realization theorem	mismatch_zero_of_realizes; approximate charge D·(τ_raw + τ_corr)	that the answering process realizes a candidate-blind kernel: sequenced settlement (timing) or factorization (isolation) are the two realizations, unchanged
92 service residual	independent	α is a property of the reference supplier; the actual supplier's departure from it is τ	unchanged
93 discovery residual	independent	β is a property of the reference repertoire	unchanged
provenance normalization	given a home, not closed	Norm_σ := subst on the move alphabet; idempotent, fixed on prohibited-free continuations; exists iff every prohibited move q uses has an authorized substitute; ShopK is the negative	the substitution's matter map is a declaration; cost is the advisor's lost gain plus the principal's lost legitimate content (silence); selection failures are not repairable by any substitution and belong to supply
inquiry causal faithfulness	split	K_E is an object; A = K_E is a transparency hypothesis	adequacy of K_E as a model of the physical experiment
free amendment	reduced	tower_factor	the fixed floor; legitimacy of Amend (episode pinning is one clause of it)
trigger integrity	reduced	T4 on the activation channel	as 89
representation adequacy	independent	the over-rich end realizes_of_injOn is its formal shadow	untouched
independent inquiry / supplier	rewritten	engine-owned selection, stopping, candidate generation, advisor-proof capacity = the engine realizes κ; exogenous costs = costs are in x not in q	evidence soundness and coverage are reference design; the theorem interface reads Realizes for the channel and the supply/discovery theorems for the reference
clause-2 receipts residual	named	class-level transparency is not log-certifiable; reference-relative transparency by re-execution is	unchanged, now the same residual for every channel

6. Countermodels

The condition run against the exact fixtures (tests/test_fixtures.py; each in its own round's interpreter) and the dispatch's list (tests/test_algebra.py, Lean Witness).

attack	fixture	x	f	transparent?	classification
hidden read in the semantics	office.hidden_reading_pair	trace	replay	no	transparency
hidden read in the effect	cases.partial_effect_pair	declared_data	trace	no (extraction_agrees = "effect differs on equal declarations")	transparency
honest hidden state	office.hidden_pair	trace	replay	yes	—
permitted persuasion	office.persuasion (+ a hidden-state variant)	trace	replay	yes; the argument is a declared finding	passes
licensed persuasion	licensed_persuasion (silent, reasoned, loud)	ltrace	Z_FIVE	yes; reasoned ≠ silent moves the machinery, loud = reasoned	passes
pressure with the trace fixed	residual_placebo	ltrace	Z_FIVE	no	transparency
unlinked split campaign	C25_split_episode(linked=False)	settlements of ancestry(E2)	licence status	no: x equal across excising E1, verdict Licensed → Unresolved	transparency, visible only under the excision counterfactual; the criterion says Licensed
linked split campaign	C25_split_episode(linked=True)	same	same	vacuous (x changes)	the criterion defeats the citation
selection read off an undeclared source	ecosystem leak, quiet world	non-advisor pre-commitment events	R	no (x blind, R not)	transparency
selection read off a declared publication	ecosystem view_prog, market world	same	R	yes, and x is not selection-blind	reference design (what the market publishes)
sealed advisor	ecosystem sealed	same	R	yes, R blind even when x is not	—
truthful cherry-picking	non-capture fixture 2	the world's true reasons	canonical content	realizes κ_first, not κ_full; every audit clause holds	selection failure: the supplier reference is not realized; charged as content d = 2, adverse mass 1/4
searching many candidates for the outlier	Lean Witness.picker	fact set	trace	not transparent as a two-element class; realizes the reference that declares its selection rule	reference design decides which selection rules are legitimate; transparency then enforces the declared one
outright false reporting	non-capture fixtures 12, 12b	—	—	voids under authentication; a certified false reason is authentication soundness	authentication (a transparency failure of the settlement channel)
hidden psychological targeting	ReasonMediatedAuthorship.Witness.covert	argument made	payload	R transparent, V not mediated	authorship
secret evaluator change	CommittedEvaluator	(occasion, declared evaluator)	score	no	transparency; impossible under re-execution
public evaluator amendment	cm5_evaluator_shedding (e0 → e1 at 60, declared)	same	score	yes	integrity/amendment (trigger design: no challenge opens)
preemptive retirement	cm2_preemptive_delicensing (licensed false from 4)	licence schedule	exposure	yes	reference design (exposure adequacy); openness of the evaluation opportunity
candidate-dependent activation	LICorrigibility.Witness.marginal_refuted	—	activation	marginal equal, joint mismatch 1/2	transparency of the activation channel (pathwise)
no authorized truthful channel	ShopK	—	—	authorship voids (η = 1); only silence normalizes; distortion 1	authority/effect completeness of the reason alphabet: the substitution has no codomain
authorized substitute exists	ShopD	—	—	lie ↦ report normalizes; W_act = 1/2, void 0	normalization exists; cost 1/2 to the advisor
omitted reason type	non-capture fixture 7, discovery rows 18–19	—	—	vacuous	representation
bounded inquiry honestly fails	discovery rows 2, 14, 17	—	—	transparent	discovery (β)
transparent threat	ReasonMediatedAuthorship fixture C	argument + threat	payload	R may be transparent, V not blind	authorship for the effect on V; the threat's execution is the effect interface
protocol self-amendment	Tower.test_tower_factor	(g, e)	spec	the authorized tower factors; an undeclared write does not	integrity/amendment (with a fixed floor)

The classification is modular in the intended sense: every attack lands in exactly one of representation, reference design, transparency, authorship, openness, discovery, service, effect/alphabet completeness, integrity/amendment, and the two ambiguous fixtures of the improvement round (CM2, CM5) split cleanly once "is the change declared?" is asked.

7. The quantitative theorem

The landed chain is U_T → U_disc → U_full with li_noncapture on each link and the discovered comparator as shared middle. The transparency defect enters as a third link in front: U_T → U_disc^A → U_disc^K → U_full, where U_disc^A is the actual supplier's docket trace and U_disc^K the reference supplier's on the same z. Each link is a MediatedPair with the same L; li_noncapture_chain's proof is asympLE_add on two li_noncaptures and admits a third verbatim. The resulting statement, with every term that cannot honestly be dropped:

E_n(U_T) − E_n(U_full)  ≲_n  L·( τ_n + α_n + β_n )  +  E_n[both·κ_n]  +  D·E_n(M_n)

• τ_n — the transparency defect in content units: the certified bound on the adverse sensitivity mass of disc^A Δ disc^K on the common-audit branch (T6 with sensitive_symmDiff in place of the width); zero under an independent supplier, which is what "independent" now means.
• α_n — the service residual, a property of the reference supplier (suffix-cut excess).
• β_n — the discovery residual, a property of the reference repertoire (cell gap).
• κ_n — the form residual, zero for an extensional program.
• M_n — the audit mismatch, ≤ τ^c_T + τ^c_disc by expect_mismatch_le_defects, zero under a content-monotone audit.

The norm is the pathwise one throughout: disagreement mass for Boolean and width-bounded payloads, expected sensitivity mass of the symmetric difference for content. Total variation appears nowhere, because the payoff algebra is pointwise in z and TV is only a lower bound on what it charges. The composition is compatible with li_noncapture, li_noncapture_chain, TraceSteering.steering_bound (which already has D·M in this position) and ReasonSupply's gated families; it is not mechanized here because the third pair needs the supply modules built, which this round did not import.

8. Lean

Built and audited: TransparentChannel.lean, importing ReasonMediatedAuthorship and LICorrigibility. Easy algebra, done: T0–T7 and the witnesses (picker, hidden_read, leak_kinds, defect_attained, tower_inhabited). Easy algebra, not done: the third chain link (T8; li_noncapture thrice) and the content form of T6 (sensitive_symmDiff composed pointwise). Genuinely new semantics, not Lean: which x the ecosystem declares (a reading of the log the round proposes as "the non-advisor pre-commitment events"); the reference κ for each channel (supplier, repertoire, registrar, answering process); the substitution alphabet of normalization; the stochastic inquiry model. Nothing is registered; the round files no claim.

9. Architecture

                 declared inputs x                    reason trace R                payload V
 (ω, q, H) ───────────────────────────► x(ω) ─── κ ───► R ─── F = eval π_P ───► V
            transparency of the           (reference-relative:      authorship (landed)
            reason channel                 Realizes β x R κ D)
            [T1: V = G ∘ x on D]

 same shape, three more channels:
   activation  c = κ_c(x, z)      candidate ∉ x        ⇒  M ≡ 0            (item 89)
   inquiry     y = K_E(ω, z)      declared kernel      ⇒  posterior = ref  (causal faithfulness)
   spec        C_{t+1} = Amend(C_t, g_t, e_t), C_0 fixed                    (free amendment)

 what each landed contract contributes:
   Integrity        the log every x, R, c, C is read off is append-only and authenticated
   Robust Openness  the reference keeps routes open under the declared interventions (K-design)
   effect completeness   every environmental influence is a declared release (the other interface)
   settlement       the reference's truth inputs are exogenous to the disposer
   authorship       V = F(R) on the audited class (the downstream half)
   transparency     R = κ(x, z) on the audited class (the upstream half)

Legitimate influence = Legitimate Evolution + Transparent Mediation, with Transparent Mediation = transparency of the reason channel + reason-mediated authorship, is mathematically natural in one exact sense: both halves are fiber invariance of a reading over the audited class, and their composite is T1. It is not a conjunct of legitimacy and should not be written as one; it is a third contract next to Non-Capture and authorship, consumed by deference. The global statement — every path from advisor-private state to the principal's normative trajectory factors through the authenticated reason interface or the authorized effect interface — is the conjunction of Realizes for the reason, activation and specification channels with effect completeness for the world channel. It does not make coercion or manufactured incentives legitimate: a transparent threat is a transparent reason with an effect behind it, and the effect interface, not this one, governs it.

What this does not establish

That any x is adequate; that any reference is well designed; that any real advisor or engine realizes its reference (EXT for the same reasons the receipts residual is EXT: a log carries one member of the audited class); that the amendment tower has a floor; that the third chain link is mechanized; that transparency by itself removes the service or discovery residuals, which are properties of the reference it is measured against. The Carroll finding depends on enrichment.excise being the world counterfactual it names. Names are provisional (AGENTS.md standard 6): Realizes, Transparent, defect, disagree, tower_factor, "transparency defect", "reference-relative / class-relative".

Deviations from the prompt

• The prompt's phrase "declared inquiry outcomes and log transforms are the evidential and counterfactual processes they name" is a paraphrase; the repository's text is the causal-contract row of FINAL_THEOREM.md §8 and the §9 wall of wiki/Corrigibility.md.
• ShopK is a fixture of the mediated-repair-dominance round, not of PRIORITIES.md; the prompt's "ShopK-style obstruction" is read as that fixture.
• Items 94–100 do not exist on main; the open pull requests #102 and #103 file 94–96 on their branches, so this round files its item as 97 to avoid a collision at merge.
• The TV formulation the prompt proposed is replaced by the pathwise disagreement mass; the prompt asked for exactly that if TV was wrong.

Outstanding maintainer actions

1. Rule on the Awaiting the author entry this round adds: whether transparent mediation enters the wiki as a named layer beside Non-Capture and authorship, and under which name.
2. Decide whether item 97 (filed here) is dispatched before or after item 89's architecture question, since T4 makes them one construction.

Transparent channel (2026-09-24)

REALIZATION-SUCCEEDS-ON-THE-ACTIVATION-AND-REASON-CHANNELS-AND-THE-EXPORTABLE-CONTRACT-IS-REFERENCE-FIDELITY — in the landed evaluation ecosystem the activation channel realizes its reference for every log because activation and payload are readings of the prefix through the commit event, so item 89's sealed comparison is the checkable log condition that the two candidates' logs agree through the commit, under which the directional mismatch is empty and without which it is attained; the reason channel's declared input is the advisor's permitted view, the non-advisor pre-commitment events, with the whole log vacuous and the empty view opaque to honest persuasion, its reference is the admitted view plus the advisor's declared program on the view, every trace program is extensional on the multiset trace, and the channel realizes its reference exactly when the advisor's contribution is its declared program's output, from which clause 6 of item 87 follows given a selection-blind view, so clause 6 reduces to an advisor-mandate event and no pre-commit publication of the selection; the specification channel has depth zero and a secret evaluator change is a realization failure the builder voids; the three-link chain is mechanized as the landed non-capture theorem applied three times with the content defect, the sensitivity mass of the symmetric difference between actual and reference content, as the first link's certified quantity, zero under fidelity, so manipulation is charged apart from service and discovery; the existential notion is vacuous or false on the reason channel without the declaration, so the contract to export is reference fidelity and canonicalization waits on the mandate event, with the activation-locality lemma promoted to item 89's row.

First pass (retained in REPORT.md): TRANSPARENCY-IS-THE-UPSTREAM-HALF-OF-AUTHORSHIP-AND-THE-SAME-PRIMITIVE — transparency of a channel to its declared inputs is fiber invariance over the audited class at a fixed exterior, the primitive of reason mediation with the declared-input view in the reason view's place and a publicly declared reference in the factor map's; class-relative transparency is the existence of some reference the class realizes and reference-relative transparency is that reference declared, the form the committed principal program, the registrar's routing and the declared log transforms already use; composed with authorship it gives oracle replacement, and it discharges item 87 clause 6 and the zero mismatch of item 89 as corollaries of a selection-blind declared-input view plus a realized reference, the pathwise form being necessary because equality of marginals leaves the joint mismatch at D/2; the approximate form is the pathwise disagreement mass, of which total variation is only a lower bound, and it enters the landed inequalities where the mismatch and content terms already sit, so the steering advantage is bounded by transparency defect plus service plus discovery residuals with no new norm; Priority 68's condition is transparency over the frame's re-simulated variation class, no record-internal condition can replace it and the unlinked split-episode arm is the witness; provenance normalization is the reason-side corrigibilization, a substitution on the move alphabet whose existence is the truthful completeness of the authorized alphabet and which cannot repair selection failures; pre-demonstration suppression and evaluator shedding are public amendments of the reference and so reference-design and trigger-design questions, their secret variants transparency failures; free amendment and trigger integrity are transparency of the specification and activation channels above a fixed floor; representation adequacy, reference design and the realization of the reference stay external.

Reading order: [ECOSYSTEM_REALIZATION.md](ECOSYSTEM_REALIZATION.md) (the second pass: the view, the three references, the realization theorems, the three-link chain, the decomposition of independence, the vocabulary decision, the loose ends), then [REPORT.md](REPORT.md) (the first pass: the primitive, the abstract theorem spine, the countermodels, the quantitative form). Lean: lean/Workspace/Deference/Contrib/TransparentChannel.lean (28 audited declarations, first pass), TransparentEcosystem.lean (22) and TransparentChain.lean (6), importing the landed ReasonMediatedAuthorship.lean, LICorrigibility.lean, EvaluationEcosystem.lean and ReasonDiscovery.lean. Fixtures: src/transparency.py, run by python3 tests/run.py (33 tests; the foreign fixtures of the legitimate-evolution, Carroll, counterfactual-legitimacy, legitimate-improvement, mediated-repair-dominance, committed-principal-program and non-capture rounds are executed in their own interpreters). Consumes ../2026-09-16-noncapture-compilation/, ../2026-09-15-li-corrigibility/, ../2026-09-10-committed-principal-program/, ../2026-09-09-mediated-repair-dominance/, ../2026-09-07-reason-mediated-authorship/, and the legitimacy rounds named above. Nothing is registered; item 97 is filed and annotated.