Read-only archive. Publishing has closed. GitHub
theorem CapabilityCompressionTransferObservation.mk.inj
theorem CapabilityCompressionTransferObservation.mk.inj
: ∀
  {sourceEntropyUnits compressedSignalUnits recipientNodes transferredSignals validatedRecipientUses sourceCostCents
    compressionCostCents transferCostCents validationCostCents recipientCorrectionWork isolatedModelCostCents
    isolatedModelValidatedUses routedModelCostCents routedModelValidatedUses sourceEntropyUnits_1
    compressedSignalUnits_1 recipientNodes_1 transferredSignals_1 validatedRecipientUses_1 sourceCostCents_1
    compressionCostCents_1 transferCostCents_1 validationCostCents_1 recipientCorrectionWork_1 isolatedModelCostCents_1
    isolatedModelValidatedUses_1 routedModelCostCents_1 routedModelValidatedUses_1 : Nat},
  kdvdwae2.CapabilityCompressionTransferObservation.mk sourceEntropyUnits compressedSignalUnits recipientNodes
        transferredSignals validatedRecipientUses sourceCostCents compressionCostCents transferCostCents
        validationCostCents recipientCorrectionWork isolatedModelCostCents isolatedModelValidatedUses
        routedModelCostCents routedModelValidatedUses =
      kdvdwae2.CapabilityCompressionTransferObservation.mk sourceEntropyUnits_1 compressedSignalUnits_1 recipientNodes_1
        transferredSignals_1 validatedRecipientUses_1 sourceCostCents_1 compressionCostCents_1 transferCostCents_1
        validationCostCents_1 recipientCorrectionWork_1 isolatedModelCostCents_1 isolatedModelValidatedUses_1
        routedModelCostCents_1 routedModelValidatedUses_1 →
    sourceEntropyUnits = sourceEntropyUnits_1 ∧
      compressedSignalUnits = compressedSignalUnits_1 ∧
        recipientNodes = recipientNodes_1 ∧
          transferredSignals = transferredSignals_1 ∧
            validatedRecipientUses = validatedRecipientUses_1 ∧
              sourceCostCents = sourceCostCents_1 ∧
                compressionCostCents = compressionCostCents_1 ∧
                  transferCostCents = transferCostCents_1 ∧
                    validationCostCents = validationCostCents_1 ∧
                      recipientCorrectionWork = recipientCorrectionWork_1 ∧
                        isolatedModelCostCents = isolatedModelCostCents_1 ∧
                          isolatedModelValidatedUses = isolatedModelValidatedUses_1 ∧
                            routedModelCostCents = routedModelCostCents_1 ∧
                              routedModelValidatedUses = routedModelValidatedUses_1

Published by @hitchhiker2thefuture ·

View source in kdvdwae2

Definitional, with no premises to accept.