OpenHCS Paper Build Log
========================

Paper: paper4d - Exact Structural Abstraction and Tractability Limits
Package Date: 2026-04-28T12:00:05.275116
Lean Toolchain: leanprover/lean4:v4.27.0-rc1

Proof Statistics:
-----------------
Lean Files: 32
Lines of Code: 23415
Theorems: 1097
Sorry Placeholders: 0


Proof Files:
------------
  - AdmissibleCharacterization.lean
  - ApproximateAdmissibility.lean
  - BinaryPairwiseDichotomy.lean
  - Block6Obstruction.lean
  - ClosureLaws.lean
  - ComputeCostApplications.lean
  - ComputeCostExternalOutputs.lean
  - ComputeCostInvariance.lean
  - ComputeCostPayloads.lean
  - DecisionRelevantPairwiseDichotomy.lean
  - DimensionalNoiseExtension.lean
  - DistinctActionProfiles.lean
  - EnumerationBounds.lean
  - ExactSpecificationNoGo.lean
  - FamilyAxioms.lean
  - FullBinaryPairwiseDomain.lean
  - MetaCharacterization.lean
  - ObstructionPredicateCandidates.lean
  - RealTreewidth.lean
  - RealTreewidthWitnesses.lean
  - Realizability.lean
  - StatisticalSemanticsApplications.lean
  - StructuralWitnesses.lean
  - TransferredFullDomainNoGo.lean
  - TreeDeletion.lean
  - TreeHellyEquivFinset.lean
  - TreeHellyFinset.lean
  - TreeHellyHelpers.lean
  - TreeHellyTheorem.lean
  - TreeLeafHelpers.lean
  - TreeLeafReduction.lean
  - TreewidthClique.lean

================================================================================
COMPILATION OUTPUT (lake build)
================================================================================

⚠ [3072/3084] Replayed Paper4dFrontier.BinaryPairwiseDichotomy
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:116:57: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  simp [DimensionalStateSpace.permute, pairState, hki,̵ ̵h̵s̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:123:54: This simp argument is unused:
  hki

Hint: Omit it from the simp argument list.
  simp [DimensionalStateSpace.permute, pairState, hki̵,̵ ̵h̵k̵j, hs, hsj]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:123:64: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  simp [DimensionalStateSpace.permute, pairState, hki, hkj, hs,̵ ̵h̵s̵j]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:123:68: This simp argument is unused:
  hsj

Hint: Omit it from the simp argument list.
  simp [DimensionalStateSpace.permute, pairState, hki, hkj, hs,̵ ̵h̵s̵j̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:174:5: unused variable `hij`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:174:19: unused variable `hpq`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:178:8: This simp argument is unused:
  r

Hint: Omit it from the simp argument list.
  simp ̵[̵r̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:215:56: This simp argument is unused:
  hpq'

Hint: Omit it from the simp argument list.
  simp [pairState, binaryCrossDifference, hpi, hqj, hp̵q'̵,̵ ̵h̵q̵i, hji]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:215:62: This simp argument is unused:
  hqi

Hint: Omit it from the simp argument list.
  simp [pairState, binaryCrossDifference, hpi, hqj, hpq', hq̵i̵,̵ ̵h̵ji]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:219:23: This simp argument is unused:
  binaryCrossDifference

Hint: Omit it from the simp argument list.
  simp [pairState, b̵i̵n̵a̵r̵y̵C̵r̵o̵s̵s̵D̵i̵f̵f̵e̵r̵e̵n̵c̵e̵,̵ ̵hpi, hqj, hqi]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:228:23: This simp argument is unused:
  binaryCrossDifference

Hint: Omit it from the simp argument list.
  simp [pairState, b̵i̵n̵a̵r̵y̵C̵r̵o̵s̵s̵D̵i̵f̵f̵e̵r̵e̵n̵c̵e̵,̵ ̵hpi, hqj, hqi]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:234:25: This simp argument is unused:
  binaryCrossDifference

Hint: Omit it from the simp argument list.
  simp [pairState, b̵i̵n̵a̵r̵y̵C̵r̵o̵s̵s̵D̵i̵f̵f̵e̵r̵e̵n̵c̵e̵,̵ ̵hpi, hpj, hpj', hqi]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:234:58: This simp argument is unused:
  hpj'

Hint: Omit it from the simp argument list.
  simp [pairState, binaryCrossDifference, hpi, hpj, hp̵j̵'̵,̵ ̵h̵qi]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:237:27: This simp argument is unused:
  binaryCrossDifference

Hint: Omit it from the simp argument list.
  simp [pairState, b̵i̵n̵a̵r̵y̵C̵r̵o̵s̵s̵D̵i̵f̵f̵e̵r̵e̵n̵c̵e̵,̵ ̵hpi, hpj, hqi]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:239:27: This simp argument is unused:
  binaryCrossDifference

Hint: Omit it from the simp argument list.
  simp [pairState, b̵i̵n̵a̵r̵y̵C̵r̵o̵s̵s̵D̵i̵f̵f̵e̵r̵e̵n̵c̵e̵,̵ ̵hpi, hpj, hqi, hqj, hpq']

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:239:70: This simp argument is unused:
  hpq'

Hint: Omit it from the simp argument list.
  simp [pairState, binaryCrossDifference, hpi, hpj, hqi, hqj,̵ ̵h̵p̵q̵'̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/BinaryPairwiseDichotomy.lean:529:77: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [3073/3084] Replayed Paper4dFrontier.DecisionRelevantPairwiseDichotomy
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:168:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:189:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:198:16: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:216:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:308:12: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:323:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:331:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:339:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:347:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/DecisionRelevantPairwiseDichotomy.lean:373:10: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3105/3205] Replayed DecisionQuotient.Hardness.QBF
warning: ../proofs/DecisionQuotient/Hardness/QBF.lean:132:39: This simp argument is unused:
  Fin.ext_iff

Hint: Omit it from the simp argument list.
  simp [restrictY, y', Fin.castLT,̵ ̵F̵i̵n̵.̵e̵x̵t̵_̵i̵f̵f̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [3106/3205] Replayed DecisionQuotient.Hardness.Sigma2PExhaustive.AnchorSufficiency
warning: ../proofs/DecisionQuotient/Hardness/Sigma2PExhaustive/AnchorSufficiency.lean:176:43: This simp argument is unused:
  hφ

Hint: Omit it from the simp argument list.
  simp [qbfProblem, qbfUtility, hφ̵,̵ ̵h̵y]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/Hardness/Sigma2PExhaustive/AnchorSufficiency.lean:186:4: Try this: intro _ a'
warning: ../proofs/DecisionQuotient/Hardness/Sigma2PExhaustive/AnchorSufficiency.lean:293:16: This simp argument is unused:
  yAllFalse

Hint: Omit it from the simp argument list.
  simp [yA̵l̵l̵F̵a̵l̵s̵e̵,̵ ̵y̵Part, s0', y0]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [3107/3205] Replayed DecisionQuotient.AlgorithmComplexity
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:119:18: This simp argument is unused:
  countedAnyList

Hint: Omit it from the simp argument list.
  simp [c̵o̵u̵n̵t̵e̵d̵A̵n̵y̵L̵i̵s̵t̵,̵ ̵Counted.bind, Counted.tick, Counted.steps, hx, hrec] at ih ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:119:34: This simp argument is unused:
  Counted.bind

Hint: Omit it from the simp argument list.
  simp [countedAnyList, C̵o̵u̵n̵t̵e̵d̵.̵b̵i̵n̵d̵,̵ ̵Counted.tick, Counted.steps, hx, hrec] at ih ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:119:48: This simp argument is unused:
  Counted.tick

Hint: Omit it from the simp argument list.
  simp [countedAnyList, Counted.bind, Counted.t̵i̵c̵k̵,̵ ̵C̵o̵u̵n̵t̵e̵d̵.̵steps, hx, hrec] at ih ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:119:77: This simp argument is unused:
  hx

Hint: Omit it from the simp argument list.
  simp [countedAnyList, Counted.bind, Counted.tick, Counted.steps, hx̵,̵ ̵h̵rec] at ih ⊢

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:144:17: This simp argument is unused:
  Prod.fst

Hint: Omit it from the simp argument list.
  simp only [P̵r̵o̵d̵.̵f̵s̵t̵,̵ ̵heq']

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:169:46: This simp argument is unused:
  Prod.fst

Hint: Omit it from the simp argument list.
  simp only [Counted.pure, Counted.steps,̵ ̵P̵r̵o̵d̵.̵f̵s̵t̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:271:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:305:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/AlgorithmComplexity.lean:376:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3108/3205] Replayed Paper4dFrontier.AdmissibleCharacterization
warning: Paper4dFrontier/AdmissibleCharacterization.lean:200:47: This simp argument is unused:
  hk.ne'

Hint: Omit it from the simp argument list.
  simp [scaleSlice, scaleUtility, castState,̵ ̵h̵k̵.̵n̵e̵'̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/AdmissibleCharacterization.lean:400:39: This simp argument is unused:
  mul_left_comm

Hint: Omit it from the simp argument list.
  simp [Nat.cast_mul, mul_assoc, m̵u̵l̵_̵l̵e̵f̵t̵_̵c̵o̵m̵m̵,̵ ̵mul_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/AdmissibleCharacterization.lean:400:54: This simp argument is unused:
  mul_comm

Hint: Omit it from the simp argument list.
  simp [Nat.cast_mul, mul_assoc, mul_left_comm,̵ ̵m̵u̵l̵_̵c̵o̵m̵m̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/AdmissibleCharacterization.lean:412:39: This simp argument is unused:
  mul_left_comm

Hint: Omit it from the simp argument list.
  simp [Nat.cast_mul, mul_assoc, m̵u̵l̵_̵l̵e̵f̵t̵_̵c̵o̵m̵m̵,̵ ̵mul_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/AdmissibleCharacterization.lean:412:54: This simp argument is unused:
  mul_comm

Hint: Omit it from the simp argument list.
  simp [Nat.cast_mul, mul_assoc, mul_left_comm,̵ ̵m̵u̵l̵_̵c̵o̵m̵m̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/AdmissibleCharacterization.lean:461:6: Try `simp at hneq` instead of `simpa using hneq`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/AdmissibleCharacterization.lean:674:11: unused variable `U`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/AdmissibleCharacterization.lean:1032:40: unused variable `hClosed`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3112/3205] Replayed DecisionQuotient.DimensionalComplexity
warning: ../proofs/DecisionQuotient/DimensionalComplexity.lean:48:68: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/DimensionalComplexity.lean:51:54: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/DimensionalComplexity.lean:54:61: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/DimensionalComplexity.lean:57:49: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/DimensionalComplexity.lean:60:63: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/DimensionalComplexity.lean:63:53: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/DimensionalComplexity.lean:77:5: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/DimensionalComplexity.lean:93:66: unused variable `regime`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3113/3205] Replayed DecisionQuotient.Reduction
warning: ../proofs/DecisionQuotient/Reduction.lean:140:4: Try this: intro _ a'
warning: ../proofs/DecisionQuotient/Reduction.lean:184:14: Try `simp at hi` instead of `simpa using hi`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3114/3205] Replayed DecisionQuotient.IntegrityCompetence
warning: ../proofs/DecisionQuotient/IntegrityCompetence.lean:326:4: Try `simp at hPos` instead of `simpa using hPos`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/IntegrityCompetence.lean:353:6: Try `simp at hPos` instead of `simpa using hPos`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/IntegrityCompetence.lean:520:44: Try `simp at hLt` instead of `simpa using hLt`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/IntegrityCompetence.lean:584:60: Try `simp at hGap` instead of `simpa using hGap`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/IntegrityCompetence.lean:617:66: Try `simp at hGap` instead of `simpa using hGap`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/IntegrityCompetence.lean:844:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3115/3205] Replayed DecisionQuotient.StochasticSequential.Basic
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:45:25: This simp argument is unused:
  Finset.sum_ite_eq

Hint: Omit it from the simp argument list.
  simp [̵F̵i̵n̵s̵e̵t̵.̵s̵u̵m̵_̵i̵t̵e̵_̵e̵q̵,̵ ̵F̵i̵n̵s̵e̵t̵.̵m̵e̵m̵_̵u̵n̵i̵v̵]̵[̲F̲i̲n̲s̲e̲t̲.̲m̲e̲m̲_̲u̲n̲i̲v̲]̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:302:4: Try this: intro ha a'
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:515:48: This simp argument is unused:
  mul_assoc

Hint: Omit it from the simp argument list.
  simp [Nat.cast_pow, pow_succ, m̵u̵l̵_̵a̵s̵s̵o̵c̵,̵ ̵mul_comm, mul_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:515:69: This simp argument is unused:
  mul_left_comm

Hint: Omit it from the simp argument list.
  simp [Nat.cast_pow, pow_succ, mul_assoc, mul_comm,̵ ̵m̵u̵l̵_̵l̵e̵f̵t̵_̵c̵o̵m̵m̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:537:36: This simp argument is unused:
  Fintype.card_fun

Hint: Omit it from the simp argument list.
  simp [Assignment, Fintype.card_f̵u̵n̵,̵ ̵F̵i̵n̵t̵y̵p̵e̵.̵c̵a̵r̵d̵_̵bool, Fintype.card_fin]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:616:25: This simp argument is unused:
  Nat.div_self (by omega : 0 < 1)

Hint: Omit it from the simp argument list.
  s̵i̵m̵p̵ ̵o̵n̵l̵y̵ ̵[̵p̵o̵w̵_̵z̵e̵r̵o̵,̵ ̵N̵a̵t̵.̵d̵i̵v̵_̵s̵e̵l̵f̵ ̵(̵b̵y̵ ̵o̵m̵e̵g̵a̵ ̵:̵ ̵0̵ ̵<̵ ̵1̵)̵]̵ ̵a̵t̵ ̵h̵s̵t̵r̵i̵c̵t̵ ̵⊢̵s̲i̲m̲p̲ ̲o̲n̲l̲y̲ ̲[̲p̲o̲w̲_̲z̲e̲r̲o̲]̲ ̲a̲t̲ ̲h̲s̲t̲r̲i̲c̲t̲
  ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲⊢̲
  ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲-̲-̲ ̲h̲s̲t̲r̲i̲c̲t̲:̲ ̲s̲a̲t̲C̲o̲u̲n̲t̲ ̲>̲ ̲0̲,̲ ̲s̲o̲ ̲s̲a̲t̲C̲o̲u̲n̲t̲ ̲≥̲ ̲1̲
  ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:797:51: unused variable `hmaj`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:831:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:1046:5: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/StochasticSequential/Basic.lean:1071:34: unused variable `r`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3116/3205] Replayed Paper4dFrontier.ComputeCostExternalOutputs
warning: Paper4dFrontier/ComputeCostExternalOutputs.lean:30:14: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3120/3205] Replayed Paper4dFrontier.SymmetryRankWitness
warning: Paper4dFrontier/SymmetryRankWitness.lean:28:59: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/SymmetryRankWitness.lean:39:59: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/SymmetryRankWitness.lean:42:24: This simp argument is unused:
  eq_comm

Hint: Omit it from the simp argument list.
  simp [h0, h1, hs,̵ ̵e̵q̵_̵c̵o̵m̵m̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/SymmetryRankWitness.lean:44:29: This simp argument is unused:
  eq_comm

Hint: Omit it from the simp argument list.
  simp [h0, h1, hs, hs',̵ ̵e̵q̵_̵c̵o̵m̵m̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/SymmetryRankWitness.lean:69:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3122/3205] Replayed Paper4dFrontier.TreeLeafHelpers
warning: Paper4dFrontier/TreeLeafHelpers.lean:64:5: unused variable `hT`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3123/3205] Replayed Paper4dFrontier.TreeDeletion
warning: Paper4dFrontier/TreeDeletion.lean:83:41: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3128/3205] Replayed Paper4dFrontier.TreewidthClique
warning: Paper4dFrontier/TreewidthClique.lean:51:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3131/3205] Replayed Paper4dFrontier.FirstTwoIndicator
warning: Paper4dFrontier/FirstTwoIndicator.lean:53:36: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3132/3205] Replayed Paper4dFrontier.SymmetryOnlyWitness
warning: Paper4dFrontier/SymmetryOnlyWitness.lean:42:47: Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/SymmetryOnlyWitness.lean:53:45: Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/SymmetryOnlyWitness.lean:56:45: Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/SymmetryOnlyWitness.lean:143:51: Try `simp at h` instead of `simpa using h`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3136/3205] Replayed Paper4dFrontier.ParentTreewidth
warning: Paper4dFrontier/ParentTreewidth.lean:68:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/ParentTreewidth.lean:68:25: 'rw [hx]' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Paper4dFrontier/ParentTreewidth.lean:68:34: 'simp' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Paper4dFrontier/ParentTreewidth.lean:68:25: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Paper4dFrontier/ParentTreewidth.lean:68:34: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Paper4dFrontier/ParentTreewidth.lean:179:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/ParentTreewidth.lean:264:14: Try `simp at ht` instead of `simpa using ht`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/ParentTreewidth.lean:255:5: unused variable `hpt`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3139/3205] Replayed DecisionQuotient.Tractability.FiniteTopK
warning: ../proofs/DecisionQuotient/Tractability/FiniteTopK.lean:46:0: automatically included section variable(s) unused in theorem `DecisionQuotient.Tractability.FiniteTopK.mem_topKWithTies_iff`:
  [DecidableEq A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: ../proofs/DecisionQuotient/Tractability/FiniteTopK.lean:54:0: automatically included section variable(s) unused in theorem `DecisionQuotient.Tractability.FiniteTopK.mem_topKList_iff`:
  [DecidableEq A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: ../proofs/DecisionQuotient/Tractability/FiniteTopK.lean:63:0: automatically included section variable(s) unused in theorem `DecisionQuotient.Tractability.FiniteTopK.mem_survivorSet_iff`:
  [DecidableEq A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [3142/3205] Replayed DecisionQuotient.Tractability.CertifiedPruning
warning: DecisionQuotient/Tractability/CertifiedPruning.lean:54:0: automatically included section variable(s) unused in theorem `DecisionQuotient.Tractability.CertifiedPruning.PruningCertificate.mem_survivors_of_mem_exactTopK`:
  [Fintype A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: DecisionQuotient/Tractability/CertifiedPruning.lean:152:0: automatically included section variable(s) unused in theorem `DecisionQuotient.Tractability.CertifiedPruning.score_selection_gap_witness_of_topK_miss`:
  [DecidableEq A]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq A] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [3145/3205] Replayed DecisionQuotient.Tractability.StructuralRank
warning: ../proofs/DecisionQuotient/Tractability/StructuralRank.lean:161:40: unused variable `hn`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Tractability/StructuralRank.lean:172:40: This simp argument is unused:
  Finset.card_fin

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.srank, hfilter,̵ ̵F̵i̵n̵s̵e̵t̵.̵c̵a̵r̵d̵_̵f̵i̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: ../proofs/DecisionQuotient/Tractability/StructuralRank.lean:223:49: unused variable `hn`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3148/3205] Replayed DecisionQuotient.ThermodynamicLift
warning: ../proofs/DecisionQuotient/ThermodynamicLift.lean:79:5: unused variable `hkB`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/ThermodynamicLift.lean:79:20: unused variable `hT`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/ThermodynamicLift.lean:96:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: ../proofs/DecisionQuotient/ThermodynamicLift.lean:135:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3149/3205] Replayed DecisionQuotient.Tractability.EpsilonUtilityGap
warning: DecisionQuotient/Tractability/EpsilonUtilityGap.lean:79:13: unused variable `hδ`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Tractability/EpsilonUtilityGap.lean:80:5: unused variable `hStrict`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3150/3205] Replayed DecisionQuotient.Tractability.MolecularSrank
warning: DecisionQuotient/Tractability/MolecularSrank.lean:111:5: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3157/3205] Replayed Paper4dFrontier.ApproximateAdmissibility
warning: Paper4dFrontier/ApproximateAdmissibility.lean:63:29: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Paper4dFrontier/ApproximateAdmissibility.lean:75:31: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3158/3205] Replayed Paper4dFrontier.SeparableOnlyWitness
warning: Paper4dFrontier/SeparableOnlyWitness.lean:58:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/SeparableOnlyWitness.lean:61:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3162/3205] Replayed DecisionQuotient.UniverseObjective
warning: ../proofs/DecisionQuotient/UniverseObjective.lean:145:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3167/3205] Replayed Paper4dFrontier.Realizability
warning: Paper4dFrontier/Realizability.lean:325:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Realizability.lean:648:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Realizability.lean:661:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Realizability.lean:696:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Realizability.lean:743:8: unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/Realizability.lean:755:8: unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/Realizability.lean:789:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Realizability.lean:793:6: unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/Realizability.lean:806:6: unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/Realizability.lean:819:6: unused variable `P`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/Realizability.lean:857:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3169/3205] Replayed Paper4dFrontier.DimensionalNoiseExtension
warning: Paper4dFrontier/DimensionalNoiseExtension.lean:110:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3170/3205] Replayed Paper4dFrontier.Block6Obstruction
warning: Paper4dFrontier/Block6Obstruction.lean:126:34: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:127:22: This simp argument is unused:
  hnotlt

Hint: Omit it from the simp argument list.
  simp [hi0, hj0, h̵n̵o̵t̵l̵t̵,̵ ̵completePairIndicator]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:127:30: This simp argument is unused:
  completePairIndicator

Hint: Omit it from the simp argument list.
  simp [hi0, hj0, hnotlt,̵ ̵c̵o̵m̵p̵l̵e̵t̵e̵P̵a̵i̵r̵I̵n̵d̵i̵c̵a̵t̵o̵r̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:150:40: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:155:42: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:168:17: This simp argument is unused:
  i1

Hint: Omit it from the simp argument list.
  simp [s, i0, i̵1̵,̵ ̵n]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:173:10: This simp argument is unused:
  i0

Hint: Omit it from the simp argument list.
  simp [i0̵,̵ ̵i̵1, n]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:212:21: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵c̵o̵n̵s̵t̵a̵n̵t̵G̵a̵p̵C̵o̵m̵p̵l̵e̵t̵e̵P̵r̵o̵b̵l̵e̵m̵,̵[̲c̲o̲n̲s̲t̲a̲n̲t̲G̲a̲p̲C̲o̲m̲p̲l̲e̲t̲e̲P̲r̲o̲b̲l̲e̲m̲,̲ constantGapCompleteProblemUtility]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:213:43: 'linarith' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Paper4dFrontier/Block6Obstruction.lean:213:43: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Paper4dFrontier/Block6Obstruction.lean:219:8: This simp argument is unused:
  DecisionProblem.Opt

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵O̵p̵t̵,̵ ̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵[̲D̲e̲c̲i̲s̲i̲o̲n̲P̲r̲o̲b̲l̲e̲m̲.̲i̲s̲O̲p̲t̲i̲m̲a̲l̲,̲ constantGapCompleteProblem,
      constantGapCompleteProblemUtility] at h

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:219:29: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.Opt, D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵constantGapCompleteProblem, constantGapCompleteProblemUtility] at h

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: Paper4dFrontier/Block6Obstruction.lean:263:78: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: Paper4dFrontier/Block6Obstruction.lean:263:74: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: Paper4dFrontier/Block6Obstruction.lean:296:62: Try this:
  [apply] ring_nf
  
  The `ring` tactic failed to close the goal. Use `ring_nf` to obtain a normal form.
    
  Note that `ring` works primarily in *commutative* rings. If you have a noncommutative ring, abelian group or module, consider using `noncomm_ring`, `abel` or `module` instead.
warning: Paper4dFrontier/Block6Obstruction.lean:296:58: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Paper4dFrontier/Block6Obstruction.lean:330:34: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:331:22: This simp argument is unused:
  hnotlt

Hint: Omit it from the simp argument list.
  simp [hi0, hj0, h̵n̵o̵t̵l̵t̵,̵ ̵completePairIndicatorReal]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:331:30: This simp argument is unused:
  completePairIndicatorReal

Hint: Omit it from the simp argument list.
  simp [hi0, hj0, hnotlt,̵ ̵c̵o̵m̵p̵l̵e̵t̵e̵P̵a̵i̵r̵I̵n̵d̵i̵c̵a̵t̵o̵r̵R̵e̵a̵l̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:387:40: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:392:42: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:411:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:420:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:442:10: This simp argument is unused:
  DecisionProblem.Opt

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.O̵p̵t̵,̵ ̵D̵e̵c̵isi̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵Optimal, offsetBaseAsymmetricPairProblem,
        offsetBaseAsymmetricPairProblemUtility, s1, hsum] at h

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:442:31: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.Opt, D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵offsetBaseAsymmetricPairProblem,
        offsetBaseAsymmetricPairProblemUtility, s1, hsum] at h

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:469:10: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp ̵[̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:470:10: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵o̵f̵f̵s̵e̵t̵C̵o̵l̵l̵a̵p̵s̵e̵d̵A̵s̵y̵m̵m̵e̵t̵r̵i̵c̵P̵a̵i̵r̵P̵r̵o̵b̵l̵e̵m̵,̵[̲o̲f̲f̲s̲e̲t̲C̲o̲l̲l̲a̲p̲s̲e̲d̲A̲s̲y̲m̲m̲e̲t̲r̲i̲c̲P̲a̲i̲r̲P̲r̲o̲b̲l̲e̲m̲,̲ offsetCollapsedAsymmetricPairProblemUtility]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:495:8: This simp argument is unused:
  DecisionProblem.Opt

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.O̵p̵t̵,̵ ̵D̵e̵c̵isi̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵Optimal, offsetCollapsedAsymmetricPairProblem,
      offsetCollapsedAsymmetricPairProblemUtility] at h

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:495:29: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.Opt, D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵offsetCollapsedAsymmetricPairProblem,
      offsetCollapsedAsymmetricPairProblemUtility] at h

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:552:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:688:27: This simp argument is unused:
  neverOptimalGhostProblemUtility

Hint: Omit it from the simp argument list.
  s̵i̵m̵p̵ ̵[̵n̵e̵v̵e̵r̵O̵p̵t̵i̵m̵a̵l̵G̵h̵o̵s̵t̵P̵r̵o̵b̵l̵e̵m̵U̵t̵i̵l̵i̵t̵y̵,̵ ̵h̵s̵]̵s̲i̲m̲p̲ ̲[̲h̲s̲]̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:688:60: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  simp [neverOptimalGhostProblemUtility,̵ ̵h̵s̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:694:12: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵n̵e̵v̵e̵r̵O̵p̵t̵i̵m̵a̵l̵G̵h̵o̵s̵t̵P̵r̵o̵b̵l̵e̵m̵,̵[̲n̲e̲v̲e̲r̲O̲p̲t̲i̲m̲a̲l̲G̲h̲o̲s̲t̲P̲r̲o̲b̲l̲e̲m̲,̲ neverOptimalGhostProblemUtility, hs] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:704:12: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵n̵e̵v̵e̵r̵O̵p̵t̵i̵m̵a̵l̵G̵h̵o̵s̵t̵P̵r̵o̵b̵l̵e̵m̵,̵[̲n̲e̲v̲e̲r̲O̲p̲t̲i̲m̲a̲l̲G̲h̲o̲s̲t̲P̲r̲o̲b̲l̲e̲m̲,̲ neverOptimalGhostProblemUtility, hs] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:719:12: This simp argument is unused:
  DecisionProblem.Opt

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵O̵p̵t̵,̵ ̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵[̲D̲e̲c̲i̲s̲i̲o̲n̲P̲r̲o̲b̲l̲e̲m̲.̲i̲s̲O̲p̲t̲i̲m̲a̲l̲,̲ neverOptimalGhostProblem, neverOptimalGhostProblemUtility,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲hs] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:719:33: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.Opt, D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵neverOptimalGhostProblem, neverOptimalGhostProblemUtility,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲hs] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:728:27: This simp argument is unused:
  neverOptimalGhostProblemUtility

Hint: Omit it from the simp argument list.
  s̵i̵m̵p̵ ̵[̵n̵e̵v̵e̵r̵O̵p̵t̵i̵m̵a̵l̵G̵h̵o̵s̵t̵P̵r̵o̵b̵l̵e̵m̵U̵t̵i̵l̵i̵t̵y̵,̵ ̵h̵s̵]̵s̲i̲m̲p̲ ̲[̲h̲s̲]̲

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:728:60: This simp argument is unused:
  hs

Hint: Omit it from the simp argument list.
  simp [neverOptimalGhostProblemUtility,̵ ̵h̵s̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:735:12: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵n̵e̵v̵e̵r̵O̵p̵t̵i̵m̵a̵l̵G̵h̵o̵s̵t̵P̵r̵o̵b̵l̵e̵m̵,̵[̲n̲e̲v̲e̲r̲O̲p̲t̲i̲m̲a̲l̲G̲h̲o̲s̲t̲P̲r̲o̲b̲l̲e̲m̲,̲ neverOptimalGhostProblemUtility, hs] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:988:14: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵m̵a̵r̵g̵i̵n̵M̵a̵s̵k̵i̵n̵g̵P̵r̵o̵b̵l̵e̵m̵,̵[̲m̲a̲r̲g̲i̲n̲M̲a̲s̲k̲i̲n̲g̲P̲r̲o̲b̲l̲e̲m̲,̲ marginMaskingProblemUtility, hs]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:989:14: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵m̵a̵r̵g̵i̵n̵M̵a̵s̵k̵i̵n̵g̵P̵r̵o̵b̵l̵e̵m̵,̵[̲m̲a̲r̲g̲i̲n̲M̲a̲s̲k̲i̲n̲g̲P̲r̲o̲b̲l̲e̲m̲,̲ marginMaskingProblemUtility, hs, marginMaskingConstantReal]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1000:12: This simp argument is unused:
  DecisionProblem.Opt

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵O̵p̵t̵,̵ ̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵[̲D̲e̲c̲i̲s̲i̲o̲n̲P̲r̲o̲b̲l̲e̲m̲.̲i̲s̲O̲p̲t̲i̲m̲a̲l̲,̲ marginMaskingProblem, marginMaskingProblemUtility, hs,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲marginMaskingConstantReal] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1000:33: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.Opt, D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵marginMaskingProblem, marginMaskingProblemUtility, hs,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲marginMaskingConstantReal] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:985:6: Try this: intro _ a'
warning: Paper4dFrontier/Block6Obstruction.lean:1019:12: This simp argument is unused:
  DecisionProblem.Opt

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵O̵p̵t̵,̵ ̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵[̲D̲e̲c̲i̲s̲i̲o̲n̲P̲r̲o̲b̲l̲e̲m̲.̲i̲s̲O̲p̲t̲i̲m̲a̲l̲,̲ marginMaskingProblem, marginMaskingProblemUtility, hs,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲marginMaskingConstantReal] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1019:33: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.Opt, D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵marginMaskingProblem, marginMaskingProblemUtility, hs,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲marginMaskingConstantReal] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1045:14: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵m̵a̵r̵g̵i̵n̵M̵a̵s̵k̵i̵n̵g̵P̵r̵o̵b̵l̵e̵m̵,̵[̲m̲a̲r̲g̲i̲n̲M̲a̲s̲k̲i̲n̲g̲P̲r̲o̲b̲l̲e̲m̲,̲ marginMaskingProblemUtility, hs]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1034:6: Try this: intro _ a'
warning: Paper4dFrontier/Block6Obstruction.lean:1108:40: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:1113:42: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:1132:4: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:1271:14: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp ̵[̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1282:12: This simp argument is unused:
  DecisionProblem.Opt

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵O̵p̵t̵,̵ ̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵[̲D̲e̲c̲i̲s̲i̲o̲n̲P̲r̲o̲b̲l̲e̲m̲.̲i̲s̲O̲p̲t̲i̲m̲a̲l̲,̲ dominantPairProblem, dominantPairProblemUtility,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲hsSign] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1282:33: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.Opt, D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵dominantPairProblem, dominantPairProblemUtility, hsSign] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1268:6: Try this: intro _ a'
warning: Paper4dFrontier/Block6Obstruction.lean:1302:12: This simp argument is unused:
  DecisionProblem.Opt

Hint: Omit it from the simp argument list.
  simp [̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵O̵p̵t̵,̵ ̵D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵[̲D̲e̲c̲i̲s̲i̲o̲n̲P̲r̲o̲b̲l̲e̲m̲.̲i̲s̲O̲p̲t̲i̲m̲a̲l̲,̲ dominantPairProblem, dominantPairProblemUtility,
  ̲  ̲ ̲ ̲ ̲ ̲ ̲ ̲hsSign] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1302:33: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [DecisionProblem.Opt, D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵dominantPairProblem, dominantPairProblemUtility, hsSign] at hlt

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1323:14: This simp argument is unused:
  DecisionProblem.isOptimal

Hint: Omit it from the simp argument list.
  simp [D̵e̵c̵i̵s̵i̵o̵n̵P̵r̵o̵b̵l̵e̵m̵.̵i̵s̵O̵p̵t̵i̵m̵a̵l̵,̵ ̵dominantPairProblem, dominantPairProblemUtility]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/Block6Obstruction.lean:1312:6: Try this: intro _ a'
warning: Paper4dFrontier/Block6Obstruction.lean:1418:40: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:1423:42: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/Block6Obstruction.lean:1419:30: This simp argument is unused:
  hi12

Hint: Omit it from the simp argument list.
  simp [s, hswap, i1, i2,̵ ̵h̵i̵1̵2̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [3171/3205] Replayed Paper4dFrontier.ObstructionPredicateCandidates
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:98:25: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:162:6: Try `simp at hij` instead of `simpa using hij`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:162:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:162:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:162:6: Try `simp at hij` instead of `simpa using hij`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:157:53: This simp argument is unused:
  i0

Hint: Omit it from the simp argument list.
  simp [offsetCollapsedWitnessPattern, offsetCollapsedSlice, BinaryPairwiseSlice.syntax,
          offsetCollapsedAsymmetricPairPairwise, f, σ, i0̵,̵ ̵i̵1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:157:57: This simp argument is unused:
  i1

Hint: Omit it from the simp argument list.
  simp [offsetCollapsedWitnessPattern, offsetCollapsedSlice, BinaryPairwiseSlice.syntax,
          offsetCollapsedAsymmetricPairPairwise, f, σ, i0,̵ ̵i̵1̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:168:53: This simp argument is unused:
  i0

Hint: Omit it from the simp argument list.
  simp [offsetCollapsedWitnessPattern, offsetCollapsedSlice, BinaryPairwiseSlice.syntax,
          offsetCollapsedAsymmetricPairPairwise, f, σ, i0̵,̵ ̵i̵1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:168:57: This simp argument is unused:
  i1

Hint: Omit it from the simp argument list.
  simp [offsetCollapsedWitnessPattern, offsetCollapsedSlice, BinaryPairwiseSlice.syntax,
          offsetCollapsedAsymmetricPairPairwise, f, σ, i0,̵ ̵i̵1̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:238:15: unused variable `U`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:327:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:327:76: 'simp [h]' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:327:76: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:524:81: 'ring' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:524:81: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:859:8: This simp argument is unused:
  GhostActionTwoPairCrossOneSlice

Hint: Omit it from the simp argument list.
  simp [̵G̵h̵o̵s̵t̵A̵c̵t̵i̵o̵n̵T̵w̵o̵P̵a̵i̵r̵C̵r̵o̵s̵s̵O̵n̵e̵S̵l̵i̵c̵e̵,̵ ̵p̵a̵i̵r̵C̵r̵o̵s̵s̵M̵a̵g̵n̵i̵t̵u̵d̵e̵,̵[̲p̲a̲i̲r̲C̲r̲o̲s̲s̲M̲a̲g̲n̲i̲t̲u̲d̲e̲,̲ neverOptimalGhostSlice, neverOptimalGhostPairwise, firstFin, secondFin,
      twoActionFin, binaryCrossDifference, completePairIndicator, fin2_0, fin2_1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:861:4: This simp argument is unused:
  twoActionFin

Hint: Omit it from the simp argument list.
  simp [GhostActionTwoPairCrossOneSlice, pairCrossMagnitude,
  ̵  ̵ ̵ ̵neverOptimalGhostSlice,
  ̲  ̲ ̲ ̲neverOptimalGhostPairwise, firstFin, secondFin,
  ̵  ̵ ̵ ̵t̵w̵o̵A̵c̵t̵i̵o̵n̵F̵i̵n̵,̵ ̵binaryCrossDifference, completePairIndicator,
  ̲  ̲ ̲ ̲fin2_0, fin2_1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:861:64: This simp argument is unused:
  fin2_0

Hint: Omit it from the simp argument list.
  simp [GhostActionTwoPairCrossOneSlice, pairCrossMagnitude,
  ̵  ̵ ̵ ̵neverOptimalGhostSlice,
  ̲  ̲ ̲ ̲neverOptimalGhostPairwise, firstFin, secondFin,
  ̵  ̵ ̵ ̵twoActionFin, binaryCrossDifference,
  ̲  ̲ ̲ ̲completePairIndicator, fin2_0̵,̵ ̵f̵i̵n̵2̵_̵1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:861:72: This simp argument is unused:
  fin2_1

Hint: Omit it from the simp argument list.
  simp [GhostActionTwoPairCrossOneSlice, pairCrossMagnitude,
  ̵  ̵ ̵ ̵neverOptimalGhostSlice,
  ̲  ̲ ̲ ̲neverOptimalGhostPairwise, firstFin, secondFin,
  ̵  ̵ ̵ ̵twoActionFin, binaryCrossDifference,
  ̲  ̲ ̲ ̲completePairIndicator, fin2_0,̵ ̵f̵i̵n̵2̵_̵1̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:921:77: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:952:10: This simp argument is unused:
  OffsetActionZeroPairCrossOneSlice

Hint: Omit it from the simp argument list.
  simp [̵O̵f̵f̵s̵e̵t̵A̵c̵t̵i̵o̵n̵Z̵e̵r̵o̵P̵a̵i̵r̵C̵r̵o̵s̵s̵O̵n̵e̵S̵l̵i̵c̵e̵,̵ ̵p̵a̵i̵r̵C̵r̵o̵s̵s̵M̵a̵g̵n̵i̵t̵u̵d̵e̵,̵[̲p̲a̲i̲r̲C̲r̲o̲s̲s̲M̲a̲g̲n̲i̲t̲u̲d̲e̲,̲ offsetCollapsedSlice, offsetCollapsedAsymmetricPairPairwise,
      firstFin, secondFin, binaryCrossDifference, completePairIndicator, fin2_0, fin2_1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:955:6: This simp argument is unused:
  fin2_0

Hint: Omit it from the simp argument list.
  simp [OffsetActionZeroPairCrossOneSlice, pairCrossMagnitude,
  ̵  ̵ ̵ ̵ ̵ ̵offsetCollapsedSlice,
  ̲  ̲ ̲ ̲offsetCollapsedAsymmetricPairPairwise,
  ̵  ̵ ̵ ̵ ̵ ̵firstFin, secondFin, binaryCrossDifference,
  ̲  ̲ ̲ ̲completePairIndicator,
  ̵  ̵ ̵ ̵ ̵ ̵fin2_0̵,̵ ̵f̵i̵n̵2̵_̵1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:955:14: This simp argument is unused:
  fin2_1

Hint: Omit it from the simp argument list.
  simp [OffsetActionZeroPairCrossOneSlice, pairCrossMagnitude,
  ̵  ̵ ̵ ̵ ̵ ̵offsetCollapsedSlice,
  ̲  ̲ ̲ ̲offsetCollapsedAsymmetricPairPairwise,
  ̵  ̵ ̵ ̵ ̵ ̵firstFin, secondFin, binaryCrossDifference,
  ̲  ̲ ̲ ̲completePairIndicator,
  ̵  ̵ ̵ ̵ ̵ ̵fin2_0,̵ ̵f̵i̵n̵2̵_̵1̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:956:10: This simp argument is unused:
  OffsetActionZeroPairCrossOneSlice

Hint: Omit it from the simp argument list.
  simp [̵O̵f̵f̵s̵e̵t̵A̵c̵t̵i̵o̵n̵Z̵e̵r̵o̵P̵a̵i̵r̵C̵r̵o̵s̵s̵O̵n̵e̵S̵l̵i̵c̵e̵,̵ ̵p̵a̵i̵r̵C̵r̵o̵s̵s̵M̵a̵g̵n̵i̵t̵u̵d̵e̵,̵[̲p̲a̲i̲r̲C̲r̲o̲s̲s̲M̲a̲g̲n̲i̲t̲u̲d̲e̲,̲ offsetCollapsedSlice, offsetCollapsedAsymmetricPairPairwise,
      firstFin, secondFin, binaryCrossDifference, completePairIndicator, fin2_0, fin2_1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:959:6: This simp argument is unused:
  fin2_0

Hint: Omit it from the simp argument list.
  simp [OffsetActionZeroPairCrossOneSlice, pairCrossMagnitude,
  ̵  ̵ ̵ ̵ ̵ ̵offsetCollapsedSlice,
  ̲  ̲ ̲ ̲offsetCollapsedAsymmetricPairPairwise,
  ̵  ̵ ̵ ̵ ̵ ̵firstFin, secondFin, binaryCrossDifference,
  ̲  ̲ ̲ ̲completePairIndicator,
  ̵  ̵ ̵ ̵ ̵ ̵fin2_0̵,̵ ̵f̵i̵n̵2̵_̵1]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: Paper4dFrontier/ObstructionPredicateCandidates.lean:959:14: This simp argument is unused:
  fin2_1

Hint: Omit it from the simp argument list.
  simp [OffsetActionZeroPairCrossOneSlice, pairCrossMagnitude,
  ̵  ̵ ̵ ̵ ̵ ̵offsetCollapsedSlice,
  ̲  ̲ ̲ ̲offsetCollapsedAsymmetricPairPairwise,
  ̵  ̵ ̵ ̵ ̵ ̵firstFin, secondFin, binaryCrossDifference,
  ̲  ̲ ̲ ̲completePairIndicator,
  ̵  ̵ ̵ ̵ ̵ ̵fin2_0,̵ ̵f̵i̵n̵2̵_̵1̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [3180/3205] Replayed Paper4dFrontier.BoundedActionsOnlyWitness2
warning: Paper4dFrontier/BoundedActionsOnlyWitness2.lean:70:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: Paper4dFrontier/BoundedActionsOnlyWitness2.lean:73:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3183/3205] Replayed Paper4dFrontier.CoreWitnesses
warning: Paper4dFrontier/CoreWitnesses.lean:64:2: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3186/3205] Replayed Paper4dFrontier.ClosureLaws
warning: Paper4dFrontier/ClosureLaws.lean:204:18: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
⚠ [3197/3205] Replayed DecisionQuotient.Statistics.FisherInformation
warning: DecisionQuotient/Statistics/FisherInformation.lean:222:35: This simp argument is unused:
  one_ne_zero

Hint: Omit it from the simp argument list.
  simp only [fisherScore, ne_eq, o̵n̵e̵_̵n̵e̵_̵z̵e̵r̵o̵,̵ ̵not_false_eq_true, iff_self]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: DecisionQuotient/Statistics/FisherInformation.lean:222:48: This simp argument is unused:
  not_false_eq_true

Hint: Omit it from the simp argument list.
  simp only [fisherScore, ne_eq, one_ne_zero, n̵o̵t̵_̵f̵a̵l̵s̵e̵_̵e̵q̵_̵t̵r̵u̵e̵,̵ ̵iff_self]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: DecisionQuotient/Statistics/FisherInformation.lean:222:67: This simp argument is unused:
  iff_self

Hint: Omit it from the simp argument list.
  simp only [fisherScore, ne_eq, one_ne_zero, not_false_eq_true,̵ ̵i̵f̵f̵_̵s̵e̵l̵f̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: DecisionQuotient/Statistics/FisherInformation.lean:235:5: unused variable `dp`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Statistics/FisherInformation.lean:236:5: unused variable `i`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Statistics/FisherInformation.lean:237:5: unused variable `y`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Statistics/FisherInformation.lean:366:5: unused variable `hI`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3200/3205] Replayed DecisionQuotient.Information.RateDistortion
warning: DecisionQuotient/Information/RateDistortion.lean:72:8: This simp argument is unused:
  neg_nonneg

Hint: Omit it from the simp argument list.
  simp ̵[̵n̵e̵g̵_̵n̵o̵n̵n̵e̵g̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: DecisionQuotient/Information/RateDistortion.lean:145:30: unused variable `d`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Information/RateDistortion.lean:145:58: unused variable `D`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Information/RateDistortion.lean:156:5: unused variable `hZero`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Information/RateDistortion.lean:157:5: unused variable `hPos`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Information/RateDistortion.lean:165:17: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3201/3205] Replayed DecisionQuotient.Information.RDSrank
warning: DecisionQuotient/Information/RDSrank.lean:88:0: automatically included section variable(s) unused in theorem `DecisionQuotient.Information.rate_equals_srank`:
  [DecidableEq (Fin n)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [DecidableEq (Fin n)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: DecisionQuotient/Information/RDSrank.lean:88:27: unused variable `ds`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Information/RDSrank.lean:98:0: automatically included section variable(s) unused in theorem `DecisionQuotient.Information.compression_below_srank_fails`:
  [Fintype A]
  [Fintype S]
  [DecidableEq (Fin n)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype A] [Fintype S] [DecidableEq (Fin n)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
warning: DecisionQuotient/Information/RDSrank.lean:113:12: This simp argument is unused:
  Finset.filter_eq_empty_iff

Hint: Omit it from the simp argument list.
  simp [F̵i̵n̵s̵e̵t̵.̵f̵i̵l̵t̵e̵r̵_̵e̵q̵_̵e̵m̵p̵t̵y̵_̵i̵f̵f̵,̵ ̵hnone]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: DecisionQuotient/Information/RDSrank.lean:149:0: automatically included section variable(s) unused in theorem `DecisionQuotient.Information.rate_distortion_bridge`:
  [Fintype A]
  [Fintype S]
  [DecidableEq (Fin n)]
consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
  omit [Fintype A] [Fintype S] [DecidableEq (Fin n)] in theorem ...

Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
⚠ [3202/3205] Replayed DecisionQuotient.Physics.IntegrityEquilibrium
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1067:52: unused variable `hReceived`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1168:5: unused variable `hPaid`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1357:23: unused variable `s`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1381:68: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1385:54: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1389:61: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1393:49: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1397:63: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1401:53: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1418:5: unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: ../proofs/DecisionQuotient/Physics/IntegrityEquilibrium.lean:1436:66: unused variable `regime`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3203/3205] Replayed DecisionQuotient.Physics.WassersteinIntegrity
warning: DecisionQuotient/Physics/WassersteinIntegrity.lean:109:41: unused variable `hn`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: DecisionQuotient/Physics/WassersteinIntegrity.lean:150:16: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: DecisionQuotient/Physics/WassersteinIntegrity.lean:153:16: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: DecisionQuotient/Physics/WassersteinIntegrity.lean:150:6: 'all_goals omega' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: DecisionQuotient/Physics/WassersteinIntegrity.lean:153:6: 'all_goals omega' tactic does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
Build completed successfully (3205 jobs).


================================================================================
END COMPILATION OUTPUT
================================================================================

Build Instructions:
-------------------
To verify the proofs compile:

  cd proofs/
  lake build

All theorems will be machine-verified if compilation succeeds.

Repository: https://github.com/trissim/openhcs
