AccessCommitment.lean

import Std

/- Conditional access verification, pinned Lean 4.24.0 with Std only.
   Two-team portable access mechanism; no general optimal-mechanism claim. -/
namespace AccessCommitment

structure Strategy where
  useful : Bool
  nonuseful : Bool
  deriving DecidableEq, Repr

def selective : Strategy := ⟨true,false⟩
def pooling : Strategy := ⟨true,true⟩
def quiet : Strategy := ⟨false,false⟩

/-- Eligibility already includes acceptance and the future gate. Reward is
    discounted private benefit, zero if the sponsor will not honor. -/
structure Game where
  prior : Rat
  reward : Rat
  usefulEligibility : Rat
  nonusefulEligibility : Rat
  burden : Rat
  deriving DecidableEq, Repr

structure Valid (g : Game) : Prop where
  prior0 : 0 ≤ g.prior
  prior1 : g.prior ≤ 1
  reward0 : 0 ≤ g.reward
  useful0 : 0 ≤ g.usefulEligibility
  useful1 : g.usefulEligibility ≤ 1
  nonuseful0 : 0 ≤ g.nonusefulEligibility
  nonuseful1 : g.nonusefulEligibility ≤ 1

def active (q : Rat) (a : Bool) : Rat := if a then q else 0

def rivalMass (g : Game) (p : Strategy) : Rat :=
  g.prior*active g.usefulEligibility p.useful +
    (1-g.prior)*active g.nonusefulEligibility p.nonuseful

def claimUtility (reward q cost rival : Rat) : Rat := reward*q*(1-rival/2)-cost

def submitUtility (g : Game) (useful : Bool) (rival : Strategy) : Rat :=
  claimUtility g.reward (if useful then g.usefulEligibility else g.nonusefulEligibility)
    g.burden (rivalMass g rival)

def Choice (u : Rat) (submit : Bool) : Prop := if submit then 0 ≤ u else u ≤ 0

def StrictChoice (u : Rat) (submit : Bool) : Prop := if submit then 0 < u else u < 0

def Equilibrium (g : Game) (first second : Strategy) : Prop :=
  Choice (submitUtility g true second) first.useful ∧
  Choice (submitUtility g false second) first.nonuseful ∧
  Choice (submitUtility g true first) second.useful ∧
  Choice (submitUtility g false first) second.nonuseful

def StrictEquilibrium (g : Game) (first second : Strategy) : Prop :=
  StrictChoice (submitUtility g true second) first.useful ∧
  StrictChoice (submitUtility g false second) first.nonuseful ∧
  StrictChoice (submitUtility g true first) second.useful ∧
  StrictChoice (submitUtility g false first) second.nonuseful

theorem lottery_probability (q r : Rat) : q*(1-r)+q*r/2=q*(1-r/2) := by grind

theorem total_lottery_probability (q r : Rat) :
    q*(1-r/2)+r*(1-q/2)=1-(1-q)*(1-r) := by grind

theorem lottery_capacity_bound (q r : Rat) (hq : q ≤ 1) (hr : r ≤ 1) :
    q*(1-r/2)+r*(1-q/2) ≤ 1 := by
  have h1 : 0 ≤ 1-q := by grind
  have h2 : 0 ≤ 1-r := by grind
  have hp := Rat.mul_nonneg h1 h2
  rw [total_lottery_probability]
  grind

theorem active_bounds (q : Rat) (a : Bool) (h0 : 0 ≤ q) (h1 : q ≤ 1) :
    0 ≤ active q a ∧ active q a ≤ 1 := by
  cases a
  · change (0 : Rat) ≤ 0 ∧ (0 : Rat) ≤ 1
    decide +kernel
  · exact ⟨h0,h1⟩

theorem rival_mass_bounds (g : Game) (hv : Valid g) (r : Strategy) :
    0 ≤ rivalMass g r ∧ rivalMass g r ≤ 1 := by
  have hu := active_bounds g.usefulEligibility r.useful hv.useful0 hv.useful1
  have hn := active_bounds g.nonusefulEligibility r.nonuseful hv.nonuseful0 hv.nonuseful1
  have hp : 0 ≤ 1-g.prior := by have h:=hv.prior1; grind
  have l1 := Rat.mul_nonneg hv.prior0 hu.1
  have l2 := Rat.mul_nonneg hp hn.1
  have u1 := Rat.mul_le_mul_of_nonneg_left hu.2 hv.prior0
  have u2 := Rat.mul_le_mul_of_nonneg_left hn.2 hp
  unfold rivalMass
  constructor <;> grind

theorem utility_lower (reward q cost rival : Rat)
    (hprod : 0 ≤ reward*q) (hr : rival ≤ 1) :
    reward*q/2-cost ≤ claimUtility reward q cost rival := by
  have hhalf : 0 ≤ (1/2 : Rat) := by decide +kernel
  have hscaled := Rat.mul_le_mul_of_nonneg_right hr hhalf
  have hdivide : rival*(1/2)=rival/2 := by grind
  have hone : (1 : Rat)*(1/2)=1/2 := by decide +kernel
  rw [hdivide,hone] at hscaled
  have hhalves : (1/2 : Rat)+(1/2)=1 := by decide +kernel
  have hf : (1/2 : Rat) ≤ 1-rival/2 := by grind
  have hm := Rat.mul_le_mul_of_nonneg_left hf hprod
  have he : reward*q*(1/2)=reward*q/2 := by grind
  rw [he] at hm
  unfold claimUtility
  grind

theorem utility_upper (reward q cost rival : Rat)
    (hprod : 0 ≤ reward*q) (hr : 0 ≤ rival) :
    claimUtility reward q cost rival ≤ reward*q-cost := by
  have hhalf : 0 ≤ (1/2 : Rat) := by decide +kernel
  have hscaled := Rat.mul_nonneg hr hhalf
  have hdivide : rival*(1/2)=rival/2 := by grind
  rw [hdivide] at hscaled
  have hf : 1-rival/2 ≤ (1 : Rat) := by grind
  have hm := Rat.mul_le_mul_of_nonneg_left hf hprod
  have he : reward*q*1=reward*q := by grind
  rw [he] at hm
  unfold claimUtility
  grind

/-- GENERAL uniform incentive theorem: capacity and future eligibility appear
    in the real award probability; disclosure is not rewarded by free utility. -/
theorem selective_dominance (g : Game) (hv : Valid g)
    (huseful : g.burden < g.reward*g.usefulEligibility/2)
    (hnonuseful : g.reward*g.nonusefulEligibility < g.burden)
    (r : Strategy) : 0 < submitUtility g true r ∧ submitUtility g false r < 0 := by
  have hr := rival_mass_bounds g hv r
  have hpu := Rat.mul_nonneg hv.reward0 hv.useful0
  have hpn := Rat.mul_nonneg hv.reward0 hv.nonuseful0
  have hl := utility_lower g.reward g.usefulEligibility g.burden (rivalMass g r) hpu hr.2
  have hh := utility_upper g.reward g.nonusefulEligibility g.burden (rivalMass g r) hpn hr.1
  simp only [submitUtility, if_true]
  constructor <;> grind

theorem positive_choice (u : Rat) (hu : 0 < u) (a : Bool) (h : Choice u a) :
    a=true := by
  cases a
  · unfold Choice at h; grind
  · rfl

theorem negative_choice (u : Rat) (hu : u < 0) (a : Bool) (h : Choice u a) :
    a=false := by
  cases a
  · rfl
  · unfold Choice at h; grind

theorem selective_unique (g : Game) (hv : Valid g)
    (huseful : g.burden < g.reward*g.usefulEligibility/2)
    (hnonuseful : g.reward*g.nonusefulEligibility < g.burden)
    (first second : Strategy) : Equilibrium g first second ↔
      first=selective ∧ second=selective := by
  have hd := selective_dominance g hv huseful hnonuseful
  constructor
  · intro h
    have hfu := positive_choice _ (hd second).1 _ h.1
    have hfn := negative_choice _ (hd second).2 _ h.2.1
    have hsu := positive_choice _ (hd first).1 _ h.2.2.1
    have hsn := negative_choice _ (hd first).2 _ h.2.2.2
    cases first
    cases second
    simp_all [selective]
  · rintro ⟨rfl,rfl⟩
    change 0 ≤ submitUtility g true selective ∧ submitUtility g false selective ≤ 0 ∧
      0 ≤ submitUtility g true selective ∧ submitUtility g false selective ≤ 0
    exact ⟨Rat.le_of_lt (hd selective).1,Rat.le_of_lt (hd selective).2,
      Rat.le_of_lt (hd selective).1,Rat.le_of_lt (hd selective).2⟩

theorem selective_strict (g : Game) (hv : Valid g)
    (huseful : g.burden < g.reward*g.usefulEligibility/2)
    (hnonuseful : g.reward*g.nonusefulEligibility < g.burden) :
    StrictEquilibrium g selective selective := by
  have h := selective_dominance g hv huseful hnonuseful selective
  exact ⟨h.1,h.2,h.1,h.2⟩

/-- A scarce qualified-access promise cannot overcome arbitrarily large costs. -/
theorem isolated_access_ceiling (g : Game) (hv : Valid g)
    (hc : g.reward*g.usefulEligibility ≤ g.burden) (r : Strategy) :
    submitUtility g true r ≤ 0 := by
  have hr := rival_mass_bounds g hv r
  have hp := Rat.mul_nonneg hv.reward0 hv.useful0
  have h := utility_upper g.reward g.usefulEligibility g.burden (rivalMass g r) hp hr.1
  simp only [submitUtility, if_true]
  grind

theorem identical_review_cannot_strictly_separate (g : Game)
    (he : g.usefulEligibility=g.nonusefulEligibility) (r : Strategy) :
    ¬ (0 < submitUtility g true r ∧ submitUtility g false r < 0) := by
  simp only [submitUtility, if_true]
  rw [he]
  grind

/-- Sponsor acts on the observable posterior mean, never hidden true quality. -/
theorem honor_strict_threshold (posterior outside breach : Rat) :
    outside-breach < posterior ↔ outside-posterior < breach := by grind

theorem renege_strict_threshold (posterior outside breach : Rat) :
    posterior < outside-breach ↔ breach < outside-posterior := by grind

theorem credibility_tie (posterior outside breach : Rat) :
    posterior=outside-breach ↔ breach=outside-posterior := by grind

/-- Joint sequential certificate: reporting is uniquely selective AND the
    sponsor strictly prefers honoring to its feasible breach alternative. -/
theorem credible_selective_implementation (g : Game) (hv : Valid g)
    (huseful : g.burden < g.reward*g.usefulEligibility/2)
    (hnonuseful : g.reward*g.nonusefulEligibility < g.burden)
    (posterior outside breach : Rat) (hcred : outside-posterior < breach) :
    StrictEquilibrium g selective selective ∧ outside-breach < posterior ∧
      ∀ first second, Equilibrium g first second ↔ first=selective ∧ second=selective := by
  exact ⟨selective_strict g hv huseful hnonuseful,
    (honor_strict_threshold posterior outside breach).2 hcred,
    selective_unique g hv huseful hnonuseful⟩

inductive Allocation where
  | outside | newFirst | newSecond | oldFirst | oldSecond
  deriving DecidableEq, Repr

def portableAllocation (creditFirst creditSecond passFirst passSecond coin : Bool) : Allocation :=
  if creditFirst && passFirst then
    if creditSecond && passSecond then (if coin then .newFirst else .newSecond)
    else .newFirst
  else if creditSecond && passSecond then .newSecond else .outside

theorem portable_never_old (c1 c2 p1 p2 coin : Bool) :
    portableAllocation c1 c2 p1 p2 coin ≠ .oldFirst ∧
    portableAllocation c1 c2 p1 p2 coin ≠ .oldSecond := by
  cases c1 <;> cases c2 <;> cases p1 <;> cases p2 <;> cases coin <;> decide +kernel

theorem portable_single_slot (c1 c2 p1 p2 coin : Bool) :
    ¬ (portableAllocation c1 c2 p1 p2 coin = .newFirst ∧
       portableAllocation c1 c2 p1 p2 coin = .newSecond) := by
  intro h
  have he : Allocation.newFirst=Allocation.newSecond := h.1.symm.trans h.2
  cases he

def goodAward (a : Allocation) (goodFirst goodSecond : Bool) : Prop :=
  match a with
  | .outside => True
  | .newFirst => goodFirst=true
  | .newSecond => goodSecond=true
  | .oldFirst | .oldSecond => False

/-- This conditional statement openly requires sound economic qualification.
    Fresh identity alone does not prove that an experiment is worthwhile. -/
theorem sound_gate_no_bad_award (c1 c2 p1 p2 coin good1 good2 : Bool)
    (h1 : p1=true → good1=true) (h2 : p2=true → good2=true) :
    goodAward (portableAllocation c1 c2 p1 p2 coin) good1 good2 := by
  cases c1 <;> cases c2 <;> cases p1 <;> cases p2 <;> cases coin <;>
    cases good1 <;> cases good2 <;> simp_all [portableAllocation,goodAward]

theorem false_gate_can_fund_bad_new :
    portableAllocation true false true false true = .newFirst ∧
    ¬ goodAward (portableAllocation true false true false true) false false := by
  change Allocation.newFirst=Allocation.newFirst ∧ ¬ ((false : Bool)=true)
  decide +kernel

inductive Mode where
  | binding | pledge | discretion | protectOld
  deriving DecidableEq, Repr

/-- Actual fixture primitives. Full costs and true future types remain separate
    from the reduced private reporting game used in the generic theorem. -/
structure Economy where
  prior : Rat
  alpha : Rat
  beta : Rat
  goodPrior : Rat
  sensitivity : Rat
  falsePositive : Rat
  goodValue : Rat
  badValue : Rat
  outside : Rat
  oldValue : Rat
  benefit : Rat
  burden : Rat
  usefulValue : Rat
  nonusefulHarm : Rat
  preparation : Rat
  review : Rat
  credit : Rat
  setup : Rat
  breach : Rat
  discount : Rat
  mode : Mode
  deriving DecidableEq, Repr

def goodPass (e : Economy) : Rat := e.goodPrior*e.sensitivity
def badPass (e : Economy) : Rat := (1-e.goodPrior)*e.falsePositive
def passProbability (e : Economy) : Rat := goodPass e+badPass e

def posterior (e : Economy) : Rat :=
  (goodPass e*e.goodValue+badPass e*e.badValue)/passProbability e

def honors (e : Economy) (pledgeHonor : Bool) : Bool :=
  match e.mode with
  | .binding | .protectOld => true
  | .pledge => pledgeHonor
  | .discretion => false

def acceptance (e : Economy) (useful submit : Bool) : Rat :=
  if submit then (if useful then e.alpha else e.beta) else 0

def issued (e : Economy) (useful submit : Bool) : Rat :=
  if e.mode == .discretion then 0 else acceptance e useful submit

def eligibleCredit (e : Economy) (useful submit : Bool) : Rat :=
  issued e useful submit * (if e.mode == .protectOld then 1 else passProbability e)

def reportGame (e : Economy) (pledgeHonor : Bool) : Game :=
  ⟨e.prior,(if honors e pledgeHonor then e.discount*e.benefit else 0),
    eligibleCredit e true true,eligibleCredit e false true,e.burden⟩

/-- Expected true-type awards computed using unconditional good/bad pass mass,
    avoiding division by zero at an impossible pass. No hidden type chooses
    the allocation; true value only scores the realized-outcome expectation. -/
def pairAwards (e : Economy) (h : Bool) (t u a b : Bool) : Rat × Rat × Rat :=
  let c1:=issued e t a
  let c2:=issued e u b
  let q1:=eligibleCredit e t a
  let q2:=eligibleCredit e u b
  let pairFactor:=c1*(1-q2/2)+c2*(1-q1/2)
  if honors e h then
    if e.mode == .protectOld then (0,0,pairFactor)
    else (pairFactor*goodPass e,pairFactor*badPass e,0)
  else (0,0,0)

def pairOrganization (e : Economy) (h : Bool) (t u a b : Bool) : Rat :=
  let accepted1:=acceptance e t a
  let accepted2:=acceptance e u b
  let useful:=(if t then accepted1 else 0)+(if u then accepted2 else 0)
  let nonuseful:=(if t then 0 else accepted1)+(if u then 0 else accepted2)
  let submissions:Rat:=(if a then 1 else 0)+(if b then 1 else 0)
  let credits:=issued e t a+issued e u b
  let q1:=eligibleCredit e t a
  let q2:=eligibleCredit e u b
  let anyQualified:=q1*(1-q2/2)+q2*(1-q1/2)
  let awards:=pairAwards e h t u a b
  let future:=e.outside+awards.1*(e.goodValue-e.outside)+
    awards.2.1*(e.badValue-e.outside)+awards.2.2*(e.oldValue-e.outside)
  let breach:=if e.mode == .pledge && !h then anyQualified*e.breach else 0
  useful*e.usefulValue-nonuseful*e.nonusefulHarm-
    submissions*(e.preparation+e.review)-credits*e.credit-e.setup+
    e.discount*(future-breach)

def organization (e : Economy) (h : Bool) (first second : Strategy) : Rat :=
  e.prior*e.prior*pairOrganization e h true true first.useful second.useful+
  e.prior*(1-e.prior)*pairOrganization e h true false first.useful second.nonuseful+
  (1-e.prior)*e.prior*pairOrganization e h false true first.nonuseful second.useful+
  (1-e.prior)*(1-e.prior)*pairOrganization e h false false first.nonuseful second.nonuseful

def expectedBadNew (e : Economy) (h : Bool) (first second : Strategy) : Rat :=
  e.prior*e.prior*(pairAwards e h true true first.useful second.useful).2.1+
  e.prior*(1-e.prior)*(pairAwards e h true false first.useful second.nonuseful).2.1+
  (1-e.prior)*e.prior*(pairAwards e h false true first.nonuseful second.useful).2.1+
  (1-e.prior)*(1-e.prior)*(pairAwards e h false false first.nonuseful second.nonuseful).2.1

def base : Economy :=
  ⟨1/2,1,0,1/2,1,0,3,-3,4,-4,4,1/2,2,1,1/4,1/4,1/4,1/4,0,1,.binding⟩
def credible : Economy := {base with mode:=.pledge,breach:=2}
def discretion : Economy := {base with mode:=.discretion,setup:=0}
def unbacked : Economy := {base with mode:=.pledge}
def protection : Economy := {base with mode:=.protectOld}
def displacement : Economy := {base with outside:=8}
def overhead : Economy := {base with setup:=1}
def rare : Economy := {base with goodPrior:=1/16}
def noQualification : Economy := {base with goodPrior:=0}
def falseValidation : Economy := {base with beta:=1}
def noisy : Economy := {base with falsePositive:=1/2}
def noisyPledge : Economy := {noisy with mode:=.pledge,breach:=2}
def noisyCredible : Economy := {noisy with mode:=.pledge,breach:=4}
def weak : Economy := {base with burden:=7/4}
def asymmetric : Economy := {base with burden:=15/8}
def credibilityBoundary : Economy := {base with mode:=.pledge,breach:=1}

theorem primary_unique (first second : Strategy) :
    Equilibrium (reportGame base true) first second ↔ first=selective ∧ second=selective := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem primary_strict : StrictEquilibrium (reportGame base true) selective selective := by
  unfold StrictEquilibrium StrictChoice
  decide +kernel

theorem primary_value : organization base true selective selective=73/16 := by decide +kernel

theorem credible_honors : credible.outside-credible.breach < posterior credible := by decide +kernel

theorem credible_matches_binding (first second : Strategy) :
    reportGame credible true=reportGame base true ∧
    organization credible true first second=organization base true first second := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> decide +kernel

theorem unbacked_reneges : posterior unbacked < unbacked.outside-unbacked.breach := by decide +kernel

theorem unbacked_unique (first second : Strategy) :
    Equilibrium (reportGame unbacked false) first second ↔ first=quiet ∧ second=quiet := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem discretion_unique (first second : Strategy) :
    Equilibrium (reportGame discretion false) first second ↔ first=quiet ∧ second=quiet := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem no_promise_values : organization discretion false quiet quiet=4 ∧
    organization unbacked false quiet quiet=15/4 := by decide +kernel

theorem protection_unique (first second : Strategy) :
    Equilibrium (reportGame protection true) first second ↔ first=selective ∧ second=selective := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem binding_bad_project_loss : organization protection true selective selective = -1 := by decide +kernel

theorem mandatory_cost_losses :
    organization displacement true selective selective=109/16 ∧
    organization displacement true selective selective<displacement.outside ∧
    organization overhead true selective selective=61/16 ∧
    organization overhead true selective selective<overhead.outside := by decide +kernel

theorem rare_and_absent_qualification_unique (zero : Bool) (first second : Strategy) :
    Equilibrium (reportGame (if zero then noQualification else rare) true) first second ↔
      first=quiet ∧ second=quiet := by
  cases zero <;> rcases first with ⟨a,b⟩ <;> rcases second with ⟨c,d⟩ <;>
    cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem no_qualification_releases_capacity : passProbability noQualification=0 ∧
    organization noQualification true quiet quiet=15/4 := by decide +kernel

theorem false_validation_pooling (first second : Strategy) :
    Equilibrium (reportGame falseValidation true) first second ↔ first=pooling ∧ second=pooling := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem false_validation_loss : organization falseValidation true pooling pooling=5/2 := by decide +kernel

theorem noisy_gate_unique (first second : Strategy) :
    Equilibrium (reportGame noisy true) first second ↔ first=selective ∧ second=selective := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem noisy_gate_posterior_and_loss : passProbability noisy=3/4 ∧ posterior noisy=1 ∧
    organization noisy true selective selective=203/64 ∧
    expectedBadNew noisy true selective selective=13/64 := by decide +kernel

theorem noisy_pledge_credibility :
    posterior noisyPledge < noisyPledge.outside-noisyPledge.breach ∧
    noisyCredible.outside-noisyCredible.breach < posterior noisyCredible := by decide +kernel

theorem weak_reporting_all_profiles (first second : Strategy) :
    Equilibrium (reportGame weak true) first second ↔
      (first=selective ∧ second=selective) ∨
      (first=selective ∧ second=quiet) ∨ (first=quiet ∧ second=selective) := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem asymmetric_reporting_all_profiles (first second : Strategy) :
    Equilibrium (reportGame asymmetric true) first second ↔
      (first=selective ∧ second=quiet) ∨ (first=quiet ∧ second=selective) := by
  rcases first with ⟨a,b⟩
  rcases second with ⟨c,d⟩
  cases a <;> cases b <;> cases c <;> cases d <;> unfold Equilibrium Choice <;> decide +kernel

theorem asymmetric_reporting_strict :
    StrictEquilibrium (reportGame asymmetric true) selective quiet ∧
    StrictEquilibrium (reportGame asymmetric true) quiet selective := by
  unfold StrictEquilibrium StrictChoice
  decide +kernel

theorem asymmetric_value : organization asymmetric true selective quiet=33/8 ∧
    organization asymmetric true quiet selective=33/8 := by decide +kernel

theorem credibility_boundary_witnesses :
    posterior credibilityBoundary=credibilityBoundary.outside-credibilityBoundary.breach ∧
    Equilibrium (reportGame credibilityBoundary true) selective selective ∧
    Equilibrium (reportGame credibilityBoundary false) quiet quiet ∧
    organization credibilityBoundary true selective selective=73/16 ∧
    organization credibilityBoundary false quiet quiet=15/4 := by
  unfold Equilibrium Choice
  decide +kernel


/-- Observable domain of a costly portable-access pledge. The positive pass
    condition excludes the undefined-posterior branch; the economic bounds
    ensure that the ordinary allocator genuinely prefers the same outside
    opportunity. These are validated premises, not inferred from a promise. -/
structure QualifiedPledge (e : Economy) : Prop where
  mode : e.mode = .pledge
  positivePass : 0 < passProbability e
  positivePosterior : 0 < posterior e
  costlyAccess : posterior e < e.outside

/-- ECONOMY-LEVEL bridge. One Economy supplies diagnosis acceptance, future
    gate law, private benefit, real sponsor alternatives and breach cost.
    The reduced reporting game and public posterior cannot be independently
    chosen to make the incentive and credibility comparisons look favorable.
    This verifies a selective reporting/strict-honor continuation under the
    declared information and commitment premises, not a general PBE theorem. -/
theorem economy_credible_selective_implementation (e : Economy)
    (hdomain : QualifiedPledge e)
    (hvalid : Valid (reportGame e true))
    (huseful : e.burden < (e.discount*e.benefit)*(e.alpha*passProbability e)/2)
    (hnonuseful : (e.discount*e.benefit)*(e.beta*passProbability e) < e.burden)
    (hcredible : e.outside-posterior e < e.breach) :
    honors e true = true ∧
    StrictEquilibrium (reportGame e true) selective selective ∧
    e.outside-e.breach < posterior e ∧
    ∀ first second, Equilibrium (reportGame e true) first second ↔
      first=selective ∧ second=selective := by
  have hm := hdomain.mode
  have hu : (reportGame e true).burden <
      (reportGame e true).reward*(reportGame e true).usefulEligibility/2 := by
    simpa [reportGame,honors,eligibleCredit,issued,acceptance,hm] using huseful
  have hn : (reportGame e true).reward*(reportGame e true).nonusefulEligibility <
      (reportGame e true).burden := by
    simpa [reportGame,honors,eligibleCredit,issued,acceptance,hm] using hnonuseful
  have h := credible_selective_implementation (reportGame e true) hvalid hu hn
    (posterior e) e.outside e.breach hcredible
  exact ⟨by simp [honors,hm],h.1,h.2.1,h.2.2⟩

end AccessCommitment