fix(sshx): qualify extra-work admission and release beta.56

.claude-plugin/marketplace.json

@@ -9,7 +9,7 @@
     {
       "name": "consensus-rnd",
       "description": "worker-delegated inline consensus：隔离多视角、固定真值表，无自有 daemon、GitHub 或 git 编排",
-      "version": "1.0.0-beta.55",
+      "version": "1.0.0-beta.56",
       "source": "./",
       "author": {
         "name": "auric",

.claude-plugin/plugin.json

@@ -1,7 +1,7 @@
 {
   "name": "consensus-rnd",
   "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无自有 daemon、GitHub 或 git 编排",
-  "version": "1.0.0-beta.55",
+  "version": "1.0.0-beta.56",
   "author": {
     "name": "auric",
     "email": "loning.ma@aelf.io"

.codex-plugin/plugin.json

@@ -1,6 +1,6 @@
 {
   "name": "consensus-rnd",
-  "version": "1.0.0-beta.55",
+  "version": "1.0.0-beta.56",
   "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无自有 daemon、GitHub 或 git 编排",
   "author": {
     "name": "auric",

.cursor-plugin/plugin.json

@@ -2,7 +2,7 @@
   "name": "consensus-rnd",
   "displayName": "Consensus R&D",
   "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无自有 daemon、GitHub 或 git 编排",
-  "version": "1.0.0-beta.55",
+  "version": "1.0.0-beta.56",
   "author": {
     "name": "auric",
     "email": "loning.ma@aelf.io"

README.md

@@ -57,7 +57,7 @@ The [review triplet](./skills/sshx/SKILL.md#review-triplet) applies the [review
 
 A [termination gate](./skills/sshx/SKILL.md#termination-gate) applies inside the final stage only when the host has positively declared a goal-driven continuation mechanism in the [goal contract](./skills/sshx/SKILL.md#goal-contract), and an affirmative satisfaction claim is being considered. It is not an eighth stage and grants no control over the host mechanism.
 
-Only confirmed defects against the current goal or an existing contract enter automatic repairs. Findings retain `evidence_status` and `user_goal_basis`; uncertain changes to product or permission semantics go to their owner for clarification. A user correction cancels dependent stale plan, review and repair authority while preserving history and active-job protection. See [goal corrections](./skills/sshx/SKILL.md#goal-contract) and [admission](./skills/sshx/SKILL.md#reasoning-discipline).
+Only confirmed defects against the current goal or an existing contract enter automatic repairs. Unverified objections alone authorize no repair or blocking goal-gap/abstention; bounded checks investigate unknowns only when the decision depends on them. Findings retain `evidence_status` and `user_goal_basis`; uncertain changes to product or permission semantics go to their owner for clarification. A user correction cancels dependent stale plan, review and repair authority while preserving history and active-job protection. See [goal corrections](./skills/sshx/SKILL.md#goal-contract) and [admission](./skills/sshx/SKILL.md#reasoning-discipline).
 
 ## Risks and Limits
 

README.zh-CN.md

@@ -57,7 +57,7 @@
 
 只有 host 在[目标合同](./skills/sshx/SKILL.md#goal-contract)中明确声明了目标驱动的继续执行机制，且 caller 正准备肯定目标已满足时，最后阶段内部才适用[终止闸门](./skills/sshx/SKILL.md#termination-gate)。它不是第八阶段，也不授予控制 host 机制的权限。
 
-只有违反当前目标或既有合同的已确认缺陷进入自动修复。发现项保留 `evidence_status` 与 `user_goal_basis`；涉及产品或权限语义的不确定改动向 owner 澄清。用户纠正立即撤销依赖旧方案的 plan、review 与 repair 权限，同时保留历史及 active job 保护。详见[目标纠正](./skills/sshx/SKILL.md#goal-contract)与[准入](./skills/sshx/SKILL.md#reasoning-discipline)。
+只有违反当前目标或既有合同的已确认缺陷进入自动修复。未验证的异议本身不授权修复或阻断性的 goal gap/abstain；只有决策依赖的未知项才值得进行有界核实。发现项保留 `evidence_status` 与 `user_goal_basis`；涉及产品或权限语义的不确定改动向 owner 澄清。用户纠正立即撤销依赖旧方案的 plan、review 与 repair 权限，同时保留历史及 active job 保护。详见[目标纠正](./skills/sshx/SKILL.md#goal-contract)与[准入](./skills/sshx/SKILL.md#reasoning-discipline)。
 
 ## 风险与限制
 

gemini-extension.json

@@ -1,6 +1,6 @@
 {
   "name": "consensus-rnd",
   "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无自有 daemon、GitHub 或 git 编排",
-  "version": "1.0.0-beta.55",
+  "version": "1.0.0-beta.56",
   "contextFileName": "GEMINI.md"
 }

package.json

@@ -1,6 +1,6 @@
 {
   "name": "consensus-rnd",
-  "version": "1.0.0-beta.55",
+  "version": "1.0.0-beta.56",
   "description": "worker-delegated inline consensus skills：隔离多视角、固定真值表，无自有 daemon、GitHub 或 git 编排",
   "license": "MIT",
   "author": "auric <loning.ma@aelf.io>",

skills/sshx/SKILL.md

@@ -194,7 +194,7 @@ Planning evidence must be gathered before a thinking seat settles a candidate pl
 
 Aesthetic/adversarial: give a symmetric 美不美 (is it beautiful?) verdict for each candidate approach materially weighed: the chosen, revised, or repair approach and each rejected alternative whose rejection changed the conclusion — beautiful, mixed, or ugly, earned from evidence, not a presumed indictment; a micro-variation that changed no decision needs no separate verdict. Name any specific locatable ugly defect, or state `no material defect found` when none exists; where a defect exists, state why the approach is ugly as a specific locatable defect and what the beautiful form would be. Ugly defects include leaked abstraction, duplicated source of truth, special-case, bad coupling, asymmetry, lying name, hidden intent, or unverifiable premise. The beautiful form is the smaller, symmetric, single-responsibility, single-source-of-truth, intent-revealing form that satisfies `GoalArtifact` — smaller, not maximally complete; gold-plating past `GoalArtifact` is itself an ugly defect, not beauty. Beauty judges the coherence and integrity of the form that remains; whether any element is unnecessary is `parsimony`'s question, and whether the whole intervention is worth its cost is the `worth` seat's — beauty must not become a second parsimony or worth vote.
 
-seek truth from facts: verify every factual premise against actual evidence before relying on it. Evidence examples include source artifact or line, current file contents, command result, test assertion, visible input, implementation-worker conclusion, or declared `GoalArtifact` constraint. Any assumed-not-verified premise must be explicitly marked `ASSUMED-UNVERIFIED` in `SshxResultEnvelope.conclusion` and either verified before routing, treated as a `GoalArtifact` goal gap, or used as an abstain trigger. A perspective must never silently rely on an assumed premise.
+seek truth from facts: verify every factual premise against actual evidence before relying on it (source artifact or line, command result, test assertion). Mark decision-relevant unknowns `ASSUMED-UNVERIFIED` in `SshxResultEnvelope.conclusion`: verified before routing or bounded checks; a `GoalArtifact` goal gap or abstain trigger needs a separate admitted `BlockingAuthority` basis; abstain only if no bounded check is available. Irrelevant premises warrant no investigation; unsupported premises warrant no repair. A perspective must never silently rely on an assumed premise.
 
 A mathematical conclusion binds a mechanism only when that mechanism's recorded state instantiates every hypothesis the conclusion needs. A name applied by analogy carries no blocking, convergence, or completion force. A missing or disputed instantiation is `ASSUMED-UNVERIFIED`; a false instantiation makes the conclusion inapplicable.
 

skills/sshx/formal/README.md

@@ -184,6 +184,15 @@ and termination-seat settlement all consume that judgment. Downgrade records
 retain the original words and trigger decision. `force` alone remains a partial
 conjunct judgment, never a complete blocking decision.
 
+`MarkedPremise.explicit` also qualifies uncertainty dispositions: an irrelevant
+premise needs no disposition; bounded verification requires decision relevance
+and an available bounded check. Goal-gap and abstention dispositions require a
+separate `completeAdmission` basis; abstention additionally requires that no bounded
+check is available. The theorems reject unsupported goal gaps and abstentions,
+exclude irrelevant investigation, and preserve independently admitted missing
+requirements. These are source/model correspondence checks, not live evidence of
+an operational repair bypass or proof that a confirmed label is truthful.
+
 `failed_trigger_rejected_by_every_consumer` checks the twenty existing decisions
 for every supplied input with a failed trigger, independently of prose labels;
 `admitted_basis_retained_by_every_consumer` retains every admitted basis that

skills/sshx/formal/Sshx/Reasoning/Discipline.lean

@@ -152,7 +152,7 @@ theorem beauty_ignores_cost_and_necessity (f : Form) (cost necessity : Nat) :
 
 /-! ## Seek truth from facts -/
 
--- SKILL[def]: "Evidence examples include source artifact or line, current file contents, command result, test assertion, visible input, implementation-worker conclusion, or declared `GoalArtifact` constraint."
+-- SKILL[def]: "source artifact or line, command result, test assertion"
 inductive Evidence
   | sourceArtifactOrLine (ref : String)
   | currentFileContents (path : String)
@@ -163,7 +163,7 @@ inductive Evidence
   | declaredGoalConstraint (item : String)
   deriving DecidableEq, Repr
 
--- SKILL[def]: "seek truth from facts: verify every factual premise against actual evidence before relying on it."
+-- SKILL[def]: "seek truth from facts: verify every factual premise against actual evidence before relying on it (source artifact or line, command result, test assertion)."
 structure Premise where
   claim : String
   evidence : Option Evidence
@@ -181,21 +181,118 @@ def Premise.status (p : Premise) : PremiseStatus :=
   | some e => .verified e
   | none => .assumedUnverified
 
--- SKILL[def]: "Any assumed-not-verified premise must be explicitly marked `ASSUMED-UNVERIFIED` in `SshxResultEnvelope.conclusion` and either verified before routing, treated as a `GoalArtifact` goal gap, or used as an abstain trigger."
+-- SKILL[def]: "Mark decision-relevant unknowns `ASSUMED-UNVERIFIED` in `SshxResultEnvelope.conclusion`: verified before routing or bounded checks; a `GoalArtifact` goal gap or abstain trigger needs a separate admitted `BlockingAuthority` basis; abstain only if no bounded check is available."
 inductive UnverifiedDisposition
   | verifiedBeforeRouting (e : Evidence)
+  | boundedVerification (question : String)
   | treatedAsGoalGap
   | abstainTrigger
   deriving DecidableEq, Repr
 
-/-- A marked premise carries its disposition; a verified premise needs none. -/
+/-- A confirmed `BlockingAuthority` basis is required before an unverified premise
+can block as a goal gap or abstention. Bounded investigation and abstention require that the
+verdict actually depends on the premise; a non-empty question names the bounded check. -/
 structure MarkedPremise where
   premise : Premise
   disposition : Option UnverifiedDisposition
+  blockingBasis : Option DecisionBasis
+  boundedCheckAvailable : Bool
   deriving DecidableEq, Repr
 
+def MarkedPremise.dispositionAdmitted (m : MarkedPremise) : Bool :=
+  match m.disposition with
+  | none => false
+  | some (.verifiedBeforeRouting _) => true
+  | some (.boundedVerification question) =>
+      m.premise.verdictDependsOnIt && question != "" && m.boundedCheckAvailable
+  | some .treatedAsGoalGap =>
+      m.premise.verdictDependsOnIt && m.blockingBasis.any completeAdmission
+  | some .abstainTrigger =>
+      m.premise.verdictDependsOnIt && !m.boundedCheckAvailable &&
+        m.blockingBasis.any completeAdmission
+
 def MarkedPremise.explicit (m : MarkedPremise) : Prop :=
-  m.premise.status = .assumedUnverified → m.disposition.isSome = true
+  m.premise.status = .assumedUnverified →
+    match m.disposition with
+    | none => m.premise.verdictDependsOnIt = false
+    | some _ => m.dispositionAdmitted = true
+
+-- SKILL[thm]: "Irrelevant premises warrant no investigation; unsupported premises warrant no repair."
+theorem decision_irrelevant_unverified_needs_no_disposition (m : MarkedPremise)
+    (h : m.premise.verdictDependsOnIt = false) (hnone : m.disposition = none) :
+    m.explicit := by
+  intro _
+  simp [hnone, h]
+
+theorem decision_irrelevant_cannot_investigate (m : MarkedPremise) (question : String)
+    (h : m.premise.verdictDependsOnIt = false)
+    (hd : m.disposition = some (.boundedVerification question)) :
+    m.dispositionAdmitted = false := by
+  simp [MarkedPremise.dispositionAdmitted, hd, h]
+
+theorem unverified_goal_gap_requires_admitted_basis (m : MarkedPremise)
+    (hstatus : m.premise.status = .assumedUnverified)
+    (hdisposition : m.disposition = some .treatedAsGoalGap)
+    (hexplicit : m.explicit) :
+    m.premise.verdictDependsOnIt = true ∧
+      ∃ b, m.blockingBasis = some b ∧ completeAdmission b = true := by
+  have ha : m.dispositionAdmitted = true := by
+    simpa only [hdisposition] using hexplicit hstatus
+  have hb : m.premise.verdictDependsOnIt = true ∧
+      m.blockingBasis.any completeAdmission = true := by
+    simpa only [MarkedPremise.dispositionAdmitted, hdisposition, Bool.and_eq_true] using ha
+  exact ⟨hb.1, (Option.any_eq_true _ _).mp hb.2⟩
+
+def unsupportedGoalGap : MarkedPremise :=
+  { premise := { claim := "unconfirmed premise", evidence := none, verdictDependsOnIt := true }
+    disposition := some .treatedAsGoalGap
+    blockingBasis := none
+    boundedCheckAvailable := false }
+
+theorem unsupported_goal_gap_is_not_explicit : ¬ unsupportedGoalGap.explicit := by
+  intro h
+  have hadmitted := h (by simp [unsupportedGoalGap, Premise.status])
+  simp [unsupportedGoalGap, MarkedPremise.dispositionAdmitted] at hadmitted
+
+def boundedUnknown : MarkedPremise :=
+  { premise := { claim := "unknown premise", evidence := none, verdictDependsOnIt := true }
+    disposition := some (.boundedVerification "check the decision-relevant workflow input")
+    blockingBasis := none
+    boundedCheckAvailable := true }
+
+theorem bounded_unknown_is_explicit : boundedUnknown.explicit := by
+  intro _
+  simp [boundedUnknown, MarkedPremise.dispositionAdmitted]
+
+def unresolvableUnknown : MarkedPremise :=
+  { premise := { claim := "unresolvable premise", evidence := none, verdictDependsOnIt := true }
+    disposition := some .abstainTrigger
+    blockingBasis := none
+    boundedCheckAvailable := false }
+
+theorem unsupported_abstention_is_not_explicit : ¬ unresolvableUnknown.explicit := by
+  intro h
+  have hadmitted := h (by simp [unresolvableUnknown, Premise.status])
+  simp [unresolvableUnknown, MarkedPremise.dispositionAdmitted] at hadmitted
+
+theorem admitted_unresolvable_unknown_is_explicit (p : Premise) (b : DecisionBasis)
+    (hrelevant : p.verdictDependsOnIt = true) (hadmitted : completeAdmission b = true) :
+    (MarkedPremise.mk p (some .abstainTrigger) (some b) false).explicit := by
+  intro _
+  simp [MarkedPremise.dispositionAdmitted, hrelevant, hadmitted]
+
+theorem available_check_prevents_abstention (m : MarkedPremise)
+    (h : m.boundedCheckAvailable = true) (hd : m.disposition = some .abstainTrigger) :
+    m.dispositionAdmitted = false := by
+  simp [MarkedPremise.dispositionAdmitted, hd, h]
+
+/-- An independently evidenced missing requirement retains the same admission, even
+when another premise is unknown. No majority or observed-occurrence condition is added. -/
+theorem admitted_goal_gap_is_explicit (p : Premise) (b : DecisionBasis)
+    (hrelevant : p.verdictDependsOnIt = true) (hadmitted : completeAdmission b = true) :
+    (MarkedPremise.mk p (some .treatedAsGoalGap) (some b) false).explicit := by
+  intro _
+  simp [MarkedPremise.dispositionAdmitted, hrelevant, hadmitted]
 
 -- SKILL[thm]: "A perspective must never silently rely on an assumed premise."
 /-- A premise the verdict depends on, assumed and carrying no disposition, is silent reliance
@@ -206,9 +303,9 @@ def silentReliance (m : MarkedPremise) : Prop :=
 
 theorem explicit_excludes_silent_reliance (m : MarkedPremise) (h : m.explicit) :
     ¬ silentReliance m := by
-  rintro ⟨-, hstatus, hnone⟩
+  rintro ⟨hdepends, hstatus, hnone⟩
   have := h hstatus
-  simp [hnone] at this
+  simp [hnone, hdepends] at this
 
 /-! ## Mathematical applicability -/
 

skills/sshx/tests/test_sshx_contract.py

@@ -381,6 +381,23 @@
 The earlier #1071-#1074 baseline and caller-reported carrier evidence retain their
 original scope and timing; they are not observations by this assignment.
 
+Extra-work-admission no-skill baseline (2026-11-05, before this assignment's
+source/model edits): the published `seek truth from facts` sentence permits every
+`ASSUMED-UNVERIFIED` premise to be treated as a `GoalArtifact` goal gap or an
+abstain trigger without saying that either disposition must be decision-relevant or
+pass `BlockingAuthority`. The unchanged formal projection `MarkedPremise.explicit`
+accepts a premise with no evidence, `verdictDependsOnIt=true`, and either
+`some .treatedAsGoalGap` or `some .abstainTrigger` because it checks only that a
+disposition is present. This is a local contract/model ambiguity: the existing
+`force`, `completeAdmission`, and operational consumers already require confirmed
+evidence, a sourced goal basis, both named conjuncts, and trigger grounding, so no
+live repair bypass is claimed. A source-level witness was established from the
+HEAD source and rechecked independently during recovery; this pre-edit baseline
+makes no compiled-model claim. Later compiled regressions are forward model evidence,
+not a live observation of a repair bypass. The forward check must qualify the
+dispositions while preserving confirmed actual defects and bounded checks for
+decision-relevant unknowns.
+
 ARCH-001 / TEST-1073-01 frozen repair baseline (2026-11-04): before this batch,
 the delegating caller supplied two independent compiled counterexamples against
 the dirty candidate. A confirmed, goal-sourced input with a failed trigger was
@@ -697,7 +714,7 @@
     "When a repair consumes the reserved capacity, the caller may add evaluation units after seeing "
     "the repair result so the mandatory rerun review and termination roster remain reachable."
 )
-CANONICAL_NORMATIVE_DOCUMENT_SHA256 = "f590f8a8529b03053cbcd63a2d9478ede828a1261af3d9976ddc57fd93a2f6f2"
+CANONICAL_NORMATIVE_DOCUMENT_SHA256 = "ca846cc828331f2d74e9563667a4022031f80b8f9d84fc87d41c2702087c8c9e"
 
 JsonValue: TypeAlias = None | bool | int | float | str | list["JsonValue"] | dict[str, "JsonValue"]
 GapOwnerAssignment: TypeAlias = tuple[JsonValue, JsonValue]
@@ -4269,6 +4286,14 @@ def test_sshx_baseline_evidence_is_source_owned(self) -> None:
         ).stdout.strip()
         self.assertEqual(tracked, "")
 
+    def test_extra_work_admission_baseline_is_source_owned(self) -> None:
+        baseline = __doc__ or ""
+        marker = "Extra-work-admission no-skill baseline (2026-11-05, before this assignment's"
+        self.assertIn(marker, baseline)
+        self.assertIn("`MarkedPremise.explicit`", baseline)
+        self.assertIn("no compiled-model claim", baseline)
+        self.assertIn("no\nlive repair bypass is claimed", baseline)
+
     def test_sshx_has_no_scientific_source_coupling(self) -> None:
         text = read(SKILL)
         self.assertEqual(set(formal_identifiers(text)), SSHX_CONTRACT_FORMAL_IDENTIFIERS)