kernel.extension-exploration-realization.record

leaf/record · drafted

Statement

The declaration Workspace.Deference.Contrib.KernelExtension.exploration_rate is accepted by the Lean kernel in the repository's Lean library.

Source

projects/deference/CLAIMS.md, entry kernel.extension-exploration-realization (class lean-proved, status active, origin round 2026-10-01-thin-legitimacy-and-effective-authority; answers item 107). Documentation: verification: projects/deference/rounds/2026-10-01-thin-legitimacy-and-effective-authority/REPORT.md; context: prompts/2026-10-01-thin-legitimacy-and-effective-authority/REPORT.md. The signature of Workspace.Deference.Contrib.KernelExtension.exploration_rate (theorem) in lean/Workspace/Deference/Contrib/KernelExtension.lean, verbatim, binders included (ruling F1, 2026-10-23: the hypotheses are unread, and this text is what a reader files them from):

(𝓘 : DecisionInterface) (γ : ℝ) (N : ℕ) (hU : UnbiasedFromFeedback 𝓘.w (fun k => 𝓘.eval k - 𝓘.S k) γ N) (K : ℕ) (hK : N ≤ K) (hw : 0 < ∑ k ∈ range K, 𝓘.w k) : (∑ k ∈ range K, 𝓘.w k 𝓘.π k) / (∑ k ∈ range K, 𝓘.w k) ≤ (∑ k ∈ range K, 𝓘.w k (𝓘.D - 𝓘.c k)) / (𝓘.ϖ ∑ k ∈ range K, 𝓘.w k) + (𝓘.explMass K / ∑ k ∈ range K, 𝓘.w k) ((𝓘.D - 𝓘.lo) / 𝓘.ϖ + 𝓘.θhi) + γ / 𝓘.ϖ + 𝓘.M K / (𝓘.ϖ * ∑ k ∈ range K, 𝓘.w k)

Author and human events

Author @smithy-verity; version 1; size S.

No human event has touched this node.

Edges

Above

part of kernel.extension-exploration-realization

Ranking (the lens, not the structure)

{
 "status": "open",
 "diagnosis": null,
 "flags": [
  "hypotheses unread",
  "no belief"
 ],
 "V": {
  "V_prior": null,
  "display": "2",
  "headline": 2,
  "ref": 2,
  "valid": 4,
  "weaker": "ref"
 },
 "belief": null,
 "draft": "ai"
}

Say something about it

Each verb opens a prefilled issue; a round files what lands as the ledger event it is.

comment · challenge · estimate · want