OAI/Combinatorics/SharpRamsey/Execution/
150 declarations, 0 contain sorry, 0 declared as axioms; 34 files
Files
- ContextOutput.lean 2 declarations
- ExecutedConditioning.lean 3 declarations
- ExecutedCosts.lean 2 declarations
- ExecutedDecodedSize.lean 3 declarations
- ExecutedDeletion.lean 8 declarations
- ExecutedEndpoint.lean 2 declarations
- ExecutedExpectedOutput.lean 1 declarations
- ExecutedExtraction.lean 3 declarations
- ExecutedFailureBudget.lean 4 declarations
- ExecutedFullMessage.lean 7 declarations
- ExecutedGoodTarget.lean 5 declarations
- ExecutedLawExtraction.lean 3 declarations
- ExecutedLoss.lean 12 declarations
- ExecutedMessage.lean 6 declarations
- ExecutedOutputCount.lean 6 declarations
- ExecutedOverhead.lean 3 declarations
- ExecutedPotential.lean 10 declarations
- ExecutedReplacement.lean 3 declarations
- ExecutedRetention.lean 2 declarations
- ExecutedSecondTrim.lean 10 declarations
- ExecutedSupportTrim.lean 4 declarations
- ExecutedTargetBudget.lean 1 declarations
- ExecutedTrim.lean 12 declarations
- FreshExecution.lean 9 declarations
- HighRankExtraction.lean 2 declarations
- HighRankReplacement.lean 6 declarations
- OriginalTargetLoss.lean 7 declarations
- OutputComposition.lean 2 declarations
- OutputCost.lean 1 declarations
- OutputRebase.lean 3 declarations
- PreparedOutput.lean 3 declarations
- VariableExtraction.lean 1 declarations
- VariableOutput.lean 2 declarations
- VariableRetention.lean 2 declarations